Cristian Ene

Yassine Lakhnech

Van Chan Ngo

Formal Indistinguishability extended to the Random Oracle Model

Several generic constructions for transforming one-way functions to asymmetric encryption schemes have been proposed. One-way functions only guarantee the weak secrecy of their arguments. That is, given the image by a one-way function of a random value, an adversary has only negligible probability to compute this random value. Encryption schemes must guarantee a stronger secrecy notion. They must be at least resistant against indistinguishability-attacks under chosen plaintext text (IND-CPA). Most practical constructions have been proved in the random oracle model. Such computational proofs turn out to be complex and error prone. Bana et al. have introduced Formal Indistinguishability Relations, (FIR for short) as an appropriate abstraction of computational indistinguishability. In this paper, we revisit their work and extend the notion of FIR to cope with the random oracle model on one hand and adaptive adversaries on the other hand. Indeed, when dealing with hash functions in the random oracle model and one-way functions, it is important to correctly abstract the notion of weak secrecy. Moreover, one needs to extend frames to include adversaries in order to capture security notions as IND-CPA.

To fix these problems, we consider pairs of formal indistinguishability relations and formal nonderivability relations. We provide a general framework along with general theorems, that ensure soundness of our approach and then we use our new framework to verify several examples of encryption schemes among which the construction of Bellare Rogaway and Hashed ElGamal.

Introduction

Our day-to-day lives increasingly depend upon information and our ability to manipulate it securely. That is, in a way that prevents malicious elements to subvert the available information for their own benefits. This requires solutions based on provably correct cryptographic systems (e.g., primitives and protocols). There are two main frameworks for analyzing cryptographic systems; the symbolic framework, originating from the work of Dolev and Yao [START_REF] Dolev | On the security of public key protocols[END_REF], and the computational approach, growing out of the work of [START_REF] Goldwasser | Probabilistic encryption[END_REF]. A significant amount of effort has been made in order to link both approaches and profit from the advantages of each of them. Indeed, while the symbolic approach is more amenable to automated proof methods, the computation approach can be more realistic.

In their seminal paper [START_REF] Abadi | Reconciling two views of cryptography (the computational soundness of formal encryption)[END_REF] Abadi and Rogaway investigate the link between the symbolic model on one hand and the computational model on the other hand. More precisely, they introduce an equivalence relation on terms and prove that equivalent terms correspond to indistinguishable distributions ensembles, when interpreted in the computational model. The work of Abadi and Rogaway has been extended to active adversaries and various cryptographic primitives in e.g. [START_REF] Micciancio | Soundness of formal encryption in the presence of active adversaries[END_REF][START_REF] Laud | Symmetric encryption in automatic analyses for confidentiality against adaptive adversaries[END_REF][START_REF] Cortier | Computationally sound, automated proofs for security protocols[END_REF][START_REF] Janvier | Completing the picture: Soundness of formal encryption in the presence of active adversaries[END_REF]]. An other line of work, also considering active adversaries is followed by Backes, Pfitzmann and Waidner using reactive simulatability [START_REF] Backes | Symmetric authentication within a simulatable cryptographic library[END_REF][START_REF] Backes | Symmetric encryption in a simulatable dolev-yao style cryptographic library[END_REF] and Canetti [START_REF] Canetti | Universally composable security: A new paradigm for cryptographic protocols[END_REF][START_REF] Canetti | Universally composable symbolic analysis of mutual authentication and key-exchange protocols[END_REF] using universal composability.

Related works A recently emerging branch of relating symbolic and computational models for passive adversaries is based on static equivalence from π-calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF], induced by an equational theory. Equational theories provide a framework to specify algebraic properties of the underlying signature, and hence, symbolic computations in a similar way as for abstract data types. That is, for a fixed equational theory, a term describes a computation in the symbolic model. Thus, an adversary can distinguish two terms, if he is able to come up with two computations that yield the same result when applied to one term but different results when applied to the other term. Such a pair of terms is called a test. This idea can be extended to frames, which roughly speaking are tuples of terms. Thus, a static equivalence relation is fully determined by the underlying equational theory, as two frames are statically equivalent, if there is no test that separates them. In [START_REF] Baudet | Computationally sound implementations of equational theories against passive adversaries[END_REF] Baudet, Cortier and Kremer study soundness and faithfulness of static equivalence for general equational theories and use their framework to prove soundness of exclusive or as well as certain symmetric encryptions. Abadi et al. [START_REF] Abadi | Guessing attacks and the computational soundness of static equivalence[END_REF] use static equivalence to analyze of guessing attacks.

Bana, Mohassel and Stegers [START_REF] Bana | Computational soundness of formal indistinguishability and static equivalence[END_REF] argue that even though static equivalence works well to obtain soundness results for the equational theories mentioned above, it does not work well in other important cases. Consider for instance the Decisional Diffie Hellman assumption (DDH for short) that states that the tuples (g, g a , g b , g ab ) and (g, g a , g b , g c ), where a, b, c are randomly sampled, are indistinguishable. It does not seem to be obvious to come up with an equational theory for group exponentiation such that the induced static equivalence includes this pair of tuples without including others whose computational indistinguishability is not proved to be a consequence of the DDH assumption. The static equivalence induced by the equational theory for group exponentiation proposed in [START_REF] Baudet | Computationally sound implementations of equational theories against passive adversaries[END_REF] includes the pair (g, g a , g b , g a 2 b ) and (g, g a , g b , g c ). It is unknown whether the computational indistinguishability of these two distributions can be proved under the DDH assumption. Therefore, Bana et al. propose an alternative approach to build symbolic indistinguishability relations and introduce formal indistinguishability relations (FIR). A FIR is defined as a closure of an initial set of equivalent frames with respect to simple operations which correspond to steps in proofs by reduction. This leads to a flexible symbolic equivalence relation. FIR has nice properties. In order to prove soundness of a FIR it is enough to prove soundness of the initial set of equivalences. Moreover, static equivalence is one instance of a FIR. Bana et al. show that it is possible to come up with a FIR whose soundness is equivalent to the DDH assumption.

Contributions. In this paper, we extend Bana et al.'s approach by introducing a notion of symbolic equivalence that allows us to prove security of encryption schemes symbolically. More specifically, we would like to be able to treat generic encryption schemes that transform oneway functions to IND-CPA secure encryption schemes. Therefore, three problems need to be solved. First, we need to cope with one-way functions. This is another example where static equivalence does not seem to be appropriate. Indeed, let f be a one-way function, that is, a function that is easy to compute but difficult to invert. It does not seem easy to come with a set of equations that capture the one-wayness of such a function. Consider the term f (a|b), where | is bit-string concatenation. If f is a one-way function then we know that we cannot easily compute a|b given f (a|b) for uniformly sampled a and b. However, nothing prevents us from being able to compute a for instance. Introducing equations that allow us to compute a from f (a|b), e.g., g(f (a|b)) = a, may exclude some one-way functions and does not solve the problem. For instance, nothing prevents us from computing a prefix of b (its first half for instance), a prefix of the prefix, etc..... . The second problem that needs to be solved is related to the fact that almost all practical provably secure encryption schemes are analyzed in the random oracle model. The random oracle model is an idealized model in which hash functions are randomly sampled functions. In this model, adversaries have oracle access to these functions. An important property is that if an adversary is unable to compute the value of an expression a and if H(a) has not been leaked then H(a) looks like a uniformly sampled value. Thus, we need to be able to symbolically prove that a value of a given expression a cannot be computed by any adversary. This is sometimes called weak secrecy in contrast to indistinguishability based secrecy. To cope with this problem, our notion of symbolic indistinguishability comes along with a non-derivability symbolic relation. Thus in our approach, we start from an initial pair of a non-derivability relation and a frame equivalence relation. Then, we provide rules that define a closure of this pair of relations in the spirit of Bana et al.'s work. Also in our case, soundness of the obtained relations can be checked by checking soundness of the initial relations. The third problem is related to the fact that security notions for encryption schemes such IND-CPA and real-or-random indistinguishability of cipher-text under chosen plaintext involve a generated from of active adversaries. Indeed, these security definitions correspond to two-phase games, where the adversary first computes a value, then a challenge is produced, the the adversary tries to solve the challenge. Static equivalence and FIR (as defined in [START_REF] Bana | Computational soundness of formal indistinguishability and static equivalence[END_REF]) consider only passive adversaries. To solve this problem we consider frames that include variables that correspond to adversaries. As frames are finite terms, we only have finitely many such variables. This is the reason why we only have a degenerate form of active adversaries which is enough to treat security of encryption schemes and digital signature, for instance.

The closure rules we propose in our framework are designed with the objective of minimizing the initial relations which depend on the underlying cryptographic primitives and assumptions.

We illustrate the framework by considering security proofs of the construction of Bellare and Rogaway [START_REF] Bellare | Random oracles are practical: a paradigm for designing efficient protocols[END_REF] and Hash El Gamal [START_REF] Baek | Secure length-saving elgamal encryption under the computational diffie-hellman assumption[END_REF].

Outline of the paper. In Section 2, we introduce the symbolic model used for describing generic asymmetric encryption schemes. In Section 3, we describe the computational framework and give definitions that relate the two models. In Section 4, we introduce our definition of formal indistinguishability relation and formal non-derivability relation. We also present our method for proving IND-CPA security. In Section 5, we illustrate our framework: we prove the construction of Bellare and Rogaway [START_REF] Bellare | Random oracles are practical: a paradigm for designing efficient protocols[END_REF] and Hash El Gamal [START_REF] Baek | Secure length-saving elgamal encryption under the computational diffie-hellman assumption[END_REF], and we give a sketch of the proof of encryption scheme proposed by Pointcheval in [START_REF] Hasan | Chosen-ciphertext security for any one-way cryptosystem[END_REF]. Finally, in Section 7 we conclude.

Symbolic semantics

Terms and subsitutions

A signature Σ = (S, F, H) consists of a countably infinite set of sorts S = {s, s 1 , ...}, a finite set of function symbols, F = {f, f 1 , ...}, and a finite set of oracle symbols, H = {g, h, h 1 , ...} together with arities of the form ar(f ) or ar(h) = s 1 × ... × s k → s, k ≥ 0. Symbols in F that take k = 0 as arguments are called constants. We suppose that there are three pairwise disjoint sets N , X and P. N is the set of names, X is the set of first-order variables, and P is the set of second order variables. We assume that both names and variables are sorted, that is, to each name or variable u, a sort s is assigned; we use s(s) for the sot of u. Variables p ∈ P have arities ar(p) = s 1 × ... × s k → s. We suppose that there are a countable number of names, variables and p-variables for each sort or arity.

A renaming is a bijection τ : N → N such that s(a) = s(τ (a)). As usual, we extend the notation s(T ) to denote the sort of a term T . Terms of sort s are defined by the grammar:

T ::= term of sort s |x variable x of sort s |p(T 1 , . . . , T k ) variable p of arity s(T 1 ) × ... × s(T k ) → s |n name n of sort s |f (T 1 , . . . , T k ) application of symbol f ∈ F with arity s(T 1 ) × ... × s(T k ) → s |h(T 1 , . . . , T k ) call of hash-function h ∈ H with arity s(T 1 ) × ... × s(T k ) → s
We use f n(T ), pvar(T ) and var(T ) for the set of free names, the set of p-variables and the set of variables that occur in the term T , respectively. We use meta-variables u, v, w to range over names and variables. We use st(T ) for the set of sub-terms of T , defined in the usual way:

st(u) def = {u} if u is

Definition 1 (Substitution).

A substitution σ is a mapping from variables to terms whose domain is finite and such that σ(x) = x, for each x in the domain. A substitution σ is written σ = {x 1 = T 1 , ..., x n = T n }, where dom(σ) = {x 1 , ..., x n } is its domain.

We only consider well-sorted substitutions for which x i and T i have the same sort, var(T i ) ⊆ {x 1 , . . . , x n } and there is no circular dependence x i 1 = T i 1 (. . . x i 2 . . .), x i 2 = T i 2 (. . . x i 3 . . .), . . . x i k = T i k (. . . x i 1 . . .). A substitution is called closed if all terms T i are closed. We let var(σ) = ∪ i var(T i ), pvar(σ) = ∪ i pvar(T i ), n(σ) = ∪ i f n(T i ), and extend the notations pvar(.), var(.), n(.) and st(.) to tuples and set of terms and substitutions in the obvious way. The application of a substitution σ to a term T is written as

σ(T ) = T σ. Let σ = {x 1 = T 1 , ..., x n = T n } and σ ′ = {x ′ 1 = T ′ 1 , ..., x ′ m = T ′ m } be substitutions such that dom(σ) ∩ dom(σ ′ ) = ∅. Then, σ|σ ′ denotes the sunbstitution {x 1 = T 1 , ..., x n = T n , x ′ 1 = T ′ 1 , ..., x ′ m = T ′ m }.
The abstract semantics of symbols is described by an equational theory E, that is an equivalence (denoted as = E ) which is stable with respect to application of contexts and wellsorted substitutions of variables. We further require that E is stable under renamings.

Definition 2 (Equational Theory.). An equational theory for a given signature is an equivalence relation E ⊆ T × T (written as = E in infix notation) on the set of terms such that

1. T 1 = E T 2 implies T 1 σ = E T 2 σ for every substitution σ; 2. T 1 = E T 2 implies T {x = T 1 } = E T {x = T 2 } for every term T and every variable x; 3. T 1 = E T 2 implies τ (T 1 ) = E τ (T 2 ) for every renaming τ .
All definitions from now on are given in the context of an (implicit) equational theory E.

Exemples. For instance, symmetric and deterministic encryption can be modeled by the theory E enc generated by the classical equation E enc = {dec(enc(x, y), y) = Eenc x}. A trapdoor one-way function can be modeled by the theory E ow generated by the equation E ow = {f -1 (f (x, pub(sk)), sk) = E x, }, where sk is the secret key (the trapdoor), f -1 is the inverse function of the trapdoor one-way function f , and pub(sk) is the public information, respectively.

Frames

Frames ( [START_REF] Abadi | A bisimulation method for cryptographic protocols[END_REF]) represent sequences of messages (or pieces of information) observed by an adversary. Formally: Definition 3 (Frame). A frame is an expression of the form φ = ν n.σ where σ is a wellsorted substitution, and n is n(σ), the set of all names occuring in σ. By abus of notation we also use n(φ) for n, the set of names bounded in the frame φ.

The novelty of our definition of frames consists in permitting adversaries to interact with frames using p-variables. This is necessary to be able to cope with adaptive adversaries. We note the set of frames by F.

Next, we define composition and parallel composition of frames. Let φ = ν n.{x

1 = T 1 , ..., x n = T n } and φ ′ = ν n ′ .σ be frames with n ∩ n ′ = ∅. Then, φφ ′ denotes the frame ν( n ∪ n ′ ).{x 1 = T 1 σ, ..., x n = T n σ}. Let now φ 1 = ν n 1 .σ 1 , ..., φ k = ν n k .
σ k be frames with pairwisely disjoint domains and pairwisely disjoint bounded names n i . Their parallel composition,

{φ 1 |φ 2 |...|φ n } is the frame ν( k i=1 n i ).σ 1 | • • • |σ k .
The iteration of a frame φ is the iterative composition of φ with itself until it remains unchanged : φ * = (. . . ((φ)φ) . . .)φ.

Definition 4 (Static equivalence). Let φ and φ ′ be two frames such that φ * = ν n.σ and

φ ′ * = ν n.σ ′ with σ = {x 1 = T 1 , ..., x n = T n } and σ ′ = {x 1 = T ′ 1 , ..., x n = T ′ n }.
Given the equational theory E, we say that φ and φ ′ are statically equivalent written φ = E φ ′ , if and only if

T i σ = E T ′ i σ ′ for all i.
Some obvious properties: φ = E φ ′ implies ψφ = E ψφ ′ and τ (φ) = E τ (φ ′ ) for any frames φ, φ ′ and ψ and any renaming τ .

Computational Semantics

Distributions and indistinguishability

Let us note η ∈ AE the security parameter. We are interested in analyzing generic schemes for asymmetric encryption assuming ideal hash functions. That is, we are working in the random oracle model [START_REF] Feige | Zero-knowledge proofs of identity[END_REF][START_REF] Bellare | Random oracles are practical: a paradigm for designing efficient protocols[END_REF]. Using standard notations, we write h r ← Ω to denote that h is randomly chosen from the set of functions with appropriate domain (deppendong on η). By abuse of notation, for a list

H = h 1 , • • • , h m of hash functions, we write H r ← Ω instead of the sequence h 1 r ← Ω, . . . , h m r
← Ω. We fix a finite set H = {h 1 , . . . , h n } of hash functions. We assume an arbitrary but fixed ordering on H; just to be able to switch between set-based and vector-based notation. A distribution ensemble is a countable sequence of distributions {X η } η∈AE . We only consider distribution ensembles that can be constructed in polynomial time by probabilistic algorithms that have oracle access to O = H. Given two distribution ensembles X = {X η } η∈AE and X ′ = {X ′ η } η∈AE , an algorithm A and η ∈ AE, we define the advantage of A in distinguishing X η and X ′ η as the following quantity:

Adv(A, η, X, X ′ ) = Pr[x r ← X η : A O (η, x) = 1] -Pr[x r ← X ′ η : A O (η, x) = 1].
Then, two distribution ensembles X and X ′ are called indistinguishable (denoted by X ∼ X ′ ) if for any probabilistic polynomial-time algorithm A, the advantage Adv(A, η, X, X ′ ) is negligible as a function of η, that is, for any n > 0, it become eventually smaller than η -n as η tends to infinity. We insist that all security notions we are going to use are in the ROM, where all algorithms, including adversaries, are equipped with oracle access to the hash functions.

Frames as distributions

We now give terms and frames a computational semantics parameterized by a computable implementation of the primitives in the random oracle model. Provided a set of sorts S and a set of symbols F, a computational algebra A = (S, F) consists of -a sequence of non-empty finite set of bit strings

[[s]] A = {[[s]] A,η } η∈AE with [[s]] A,η ⊆ {0, 1} *
for each sort s ∈ S. For simplicity of the presentation, we assume that all sorts are large domains, whose cardinalities are exponential in the security parameter η; -a sequence of polynomial time computable functions

[[f ]] A = {[[f ]] A,η } η∈AE with [[f ]] A,η : [[s 1 ]] A,η × ... × [[s k ]] A,η → [[s]] A,η for each f ∈ F with ar(f ) = s 1 × ... × s k → s; -a polynomial time computable congruence = A,
η,s for each sort s, in order to check the equality of elements in [[s]] A,η (the same element may be represented by different bit strings). By congruence, we mean a reflexive, symmetric, and transitive relation such that

e 1 = A,s 1 ,η e ′ 1 , ..., e k = A,s k ,η e ′ k ⇒ [[f ]] A,η (e 1 , ..., e k ) = A,s,η [[f ]] A,η (e ′ 1 , ..., e ′ k )
( we usually omit s,η and A and write = for = A,s,η ); -a polynomial time procedure to draw random elements from [[s]] A,η ; we denote such a drawing by x ← R [[s]] A,η ; for simplicity, in this paper we suppose that all these drawing follow a uniform distribution.

From now on we assume a fixed computational algebra (S, F), and a fixed η, and for simplicity we omit the indices A,s and η.

Given H a fixed set of hash functions, and (A i ) i∈I a fixed set of polynomial-probabilistc functions (can be seen as a polynomial-probabilistc adversary A O that takes an additional input i), we associate to each frame φ = ν n.{x

1 = T 1 , . . . , x k = T k } a sequence of distributions [[φ]] H,A computed as follows: -for each name n of sort s appearing in n, draw a value n r ← [[s]]; -for each variable x i (1 ≤ i ≤ k) of sort s i , compute Ti ∈ [[s i ]]
recursively on the structure of terms: xi = Ti ; -for each call h i (T ′ 1 , . . . , T ′ m ) compute recursively on the structure of terms:

h i (T ′ 1 , . . . , T ′ m ) = h i ( T ′ 1 , . . . , T ′ m ); -for each call f (T ′ 1 , . . . , T ′ m ) compute recursively on the structure of terms: f (T ′ 1 , . . . , T ′ m ) = [[f ]]( T ′ 1 , . . . , T ′ m ); -for each call p i (T ′ 1 , .
. . , T ′ m ) compute recursively on the structure of terms and draw a value

p i (T ′ 1 , . . . , T ′ m ) r ← A O (i, T ′ 1 , . . . , T ′ m );
-return the value φ = {x 1 = T1 , . . . , x k = Tk }.

Such values φ = {x 1 = bse 1 , . . . , x n = bse n } with bse i ∈ [[s i ]] are called concrete frames. We extend the notation [[.]] to (sets of) closed terms in the obvious way. We also generalize the notation to terms or frames with free variables and free names, by specifying the concrete values for all of them: [[.]] {n 1 =bsn 1 ,...n k =bsn k ,x 1 =bse 1 ,...,x l =bse l } . Now the concrete semantics of a frame φ with respect to an adversary A, is given by the following sequence of distributions (one for each implicit η):

[[φ]] A = H r ← Ω; O = H; φ r ← [[φ]] H,A : φ
When pvar(φ) = ∅, the concrete semantics of φ does not depend on the adversary A and we will use the notation

[[φ]] (or [[φ]] H ) instead of [[φ]] A (respectively [[φ]] H,A ).

Soundness and Completeness

The computational model of a cryptographic scheme is closer to reality than its formal representation by being a more detailed description. Therefore, the accuracy of a formal model can be characterized based on how close it is to the computational model. For this reason, we introduce the notions of soundness and completeness that relate relations in the symbolic model with respect to similar relations in the computational model. Let E be an equivalence theory and let R 1 ⊆ T × T, R 2 ⊆ F × T, and R 3 ⊆ F × F be relations on closed frames, on closed terms, and relations on closed frames and terms, respectively.

-

Then R 1 is =-sound iff for every closed terms T 1 , T 2 of the same sort, (T 1 , T 2 ) ∈ R 1 implies that Pr[ ê1 , ê2 r ← [[T 1 , T 2 ]] A : ê1 = ê2 ))] is negligible for any polynomial time adversary A. -Then R 1 is =-complete iff for every closed terms T 1 , T 2 of the same sort, (T 1 , T 2 ) ∈ R 1 implies that Pr[ ê1 , ê2 r ← [[T 1 , T 2 ]] A : ê1 = ê2
))] is non-negligible for some polynomial time adversary A.

-Then R 2 is ⊢-sound iff for every closed frame φ and term T , (φ,

T ) ∈ R 2 implies that Pr[ φ, ê r ← [[φ, T ]] A : A O ( φ) = ê
] is negligible for any probabilistic polynomial-time adversary A.

-Then R 2 is ⊢-complete iff for every closed frame φ and term T , (φ,

T ) ∈ R 2 implies that Pr[ φ, ê r ← [[φ, T ]] A : A O ( φ) = ê] is non-negligible for some polynomial-time adversary A. -Then R 3 is ≈ E -sound iff for every frames φ 1 , φ 2 with the same domain, (φ 1 , φ 2 ) ∈ R 3 implies that ([[φ 1 ]] A ) ∼ ([[φ 2 ]] A ) for any probabilistic polynomial-time adversary A. -Then R 3 is ≈ E -complete iff for every frames φ 1 , φ 2 with the same domain, (φ 1 , φ 2 ) ∈ R 3 implies that ([[φ 1 ]] A ) ∼ ([[φ 2 ]
] A ) for some probabilistic polynomial-time adversary A.

Formal relations

One challenge of the paper is to propose appropriate symbolic relations that correctly abstract computational properties as indistinguishability of two distributions or weak secrecy of some random value (that is, the adversary has only negligible probability to compute it). In this section we provide two symbolic relations (called formal indistinguishability relation and formal non-derivability relation) that are sound abstractions for the two above computational properties.

First we define well-formed relations and we recall a simplified definition of a formal indistinguishability relation as proposed in [START_REF] Bana | Computational soundness of formal indistinguishability and static equivalence[END_REF].

Definition 5 (Well-formed relations). A relation

S d ⊆ F × T is called well-formed if f n(M ) ⊆ n(φ) for any (φ, M ) ∈ S d , and a relation S i ⊆ F × F is well-formed if dom(φ 1 ) = dom(φ 2 ) for any (φ 1 , φ 2 ) ∈ S i . Definition 6.
[FIR [START_REF] Bana | Computational soundness of formal indistinguishability and static equivalence[END_REF]] A well-formed equivalence relation ∼ =⊆ F × F is called a formal indistinguishability relation (FIR for short) with respect to the equational theory = E , if ∼ = is closed with respect to the following closure rules:

(GE1) If φ 1 ∼ = φ 2 then φφ 1 ∼ = φφ 2 , for any frame φ such that var(φ) ⊆ dom(φ i ) and n(φ) ∩ n(φ i ) = ∅. (GE2) φ ∼ = φ ′ for any frame φ ′ such that φ ′ = E φ. (GE3) τ (φ) ∼ = φ for any renaming τ .
This definition is a good starting point to capture indistinguishability in the following sense: if we have a correct implementation of the abstract algebra (i.e. = E is =-sound) and we were provided with some initial relation S (reflecting some computational assumption) which is ≈-sound , then the closure of S using the above rules produces a larger relation which still remains ≈-sound. But in order to use this definition for real cryptographic constructions , we need to enrich it in several aspects. First, most of constructions which are proposed in the literature, ( [START_REF] Bellare | Optimal asymmetric encryption[END_REF], [START_REF] Zheng | Immunizing public key cryptosystems against chosen ciphertext attacks[END_REF], [START_REF] Okamoto | React: Rapid enhanced-security asymmetric cryptosystem transform[END_REF], [START_REF] Hasan | Chosen-ciphertext security for any one-way cryptosystem[END_REF], [START_REF] Shoup | Oaep reconsidered[END_REF], [START_REF] Bellare | Random oracles are practical: a paradigm for designing efficient protocols[END_REF]) use bijective functions (XOR-function or trapdoor permutation) as basic bricks. To deal with these constructions, we add the following closure rule:

(GE4) If M, N are terms such that N [M/z] = E y, M [N/y] = E z and var(M ) = {y} and var(N ) = {z}, then for any substitution σ such that r ∈ (f n(σ) ∪ f n(M ) ∪ f n(N )) and x ∈ dom(σ) it holds ν n.r.{σ, x = M [r/y])} ∼ = ν n.r.{σ, x = r}.
Second, cryptographic constructions use often hash functions. In ideal models, hash functions are primitives that if applied to a weakly secret argument, produce a completely random value (modeled by random functions [START_REF] Bellare | Random oracles are practical: a paradigm for designing efficient protocols[END_REF] or by pseudo-random permutations [START_REF] Duong | About the security of ciphers (semantic security and pseudorandom permutations)[END_REF]). And they are quite frequent primitives in cryptography that only ensure weak secrecy. For instance oneway functions only guarantee that an adversary that possesses the image by a one-way function of a random value, has only a negligible probability to compute this value. The computational Diffie-Hellman (CDH) assumption states that if given the tuple g, g a , g b for some randomlychosen generator g and some random values a, b, it is computationally intractable to compute the value g a * b (equivalently g a * b is a weakly secret value). This motivates us to introduce the formal non-derivability relation as an abstraction of weak secrecy. Let us explain the basic closure rules of this relation. Since we assume that all sorts will be implemented by large finite sets of bit strings, it is clearly that (GD1) νr.∅ |= r.

Next rule captures the fact that renaming does not change the concrete semantics of terms or frames.

(GD2) If φ |= M then τ (φ) |= τ (M ) for any renaming τ .
If the equational theory is preserved in the computational world, then equivalent terms or frames are indistinguishable.

(GD3) If φ |= M then φ |= N for any term N = E M . (GD4) If φ |= M then φ ′ |= M for any frame φ ′ = E φ.
If some bit string (concrete implementation of some symbolic term M ) is weakly secret, then all polynomially computation (abstracted by the symbolic frame φ ′ ) does not change this.

(GD5) If φ |= M then φ ′ φ |= M for any frame φ ′ such that var(φ ′ ) ⊆ dom(φ) and n(φ ′ ) ∩ bn(φ) = ∅.
Next rule establishes a relationship between indistiguishability and secrecy: if two distributions are indistinguishable, then they leak exactly the same information. (GD6) If T, U are terms such that U [T /y] = E z and z ∈ var(T )\var(U ) and (f n(T )∪f n(U ))∩ n = ∅, then for all substitutions σ 1 , σ 2 such that x ∈ dom(σ i ) and ν n. The following definition formalizes the tight connection between FIR and FNDR.

Definition 7 (FNDR and FIR).

A pair of well formed relations ( |=, ∼ =) is a pair of (formal non-derivability relation, formal indistinguishability relation) with respect to the equational theory = E , if ( |=, ∼ =) is closed with respect to the rules (GD1), ..., (GD6),(GE1),...,(GE4), (HE1) and ∼ = is an equivalence.

The following theorem shows that if a pair of FIR and FNDR relations was generated by the initial sets S d ⊆ F × T and S i ⊆ F × F, then it is sufficient to check only soundness of elements in S d and S i to ensure that the closures S d |= and S i ∼ = are sound. We define (D 1 , I 1 ) ⊏ (D 2 , I 2 ) if and only if D 1 ⊆ D 2 and I 1 ⊆ I 2 . It is easy to see that ⊏ is an order. Theorem 1. Let (S d , S i ) be a well-formed pair of relations. Then, it exists a unique smallest (with respect to ⊏) pair denoted

( S d |= , S i ∼ = ) of (FNDR, FIR) such that S d |= ⊇ S d and S i ∼ = ⊇ S i . In addition, if = E is =-sound, S d is ⊢-sound and S i is ≈-sound, then also S d |= is ⊢-sound and S i ∼ = is ≈-sound.

Applications

We apply the framework of Section 4 in order to prove IND-CPA security of several generic constructions for asymmetric encryptions. So we will consider pairs of relations ( |=, ∼ =) = ( S d |= , S i ∼ = ) generated by some initial sets (S d , S i ), in different equational theories. We assume that all = E , S d , S i that are considerd in this section satisfy the conditions of Theorem 1. We emphasize the following fact: adding other equations than those considered does not break the computational soundness of results proved in this section, as long as the computational hypothesis encoded by S d and S i still hold. First we introduce a general abstract algebra, and then we will extend it to cover different constructions. We consider three sorts Data, Data 1 , Data 2 , and the symbols || : Data 1 × Data 2 → Data, ⊕ S : S × S → S, 0 S : S, with S ∈ {Data, Data 1 , Data 2 } and π j : Data → Data j , with j ∈ {1, 2}. For simplicity, we omit the indice S when using ⊕ S or 0 S . The equational theory E g is generated by:

(XEq1) x ⊕ 0 = Eg x. (XEq2) x ⊕ x = Eg 0. (XEq3) x ⊕ y = Eg y ⊕ x. (XEq4) x ⊕ (y ⊕ z) = Eg (x ⊕ y) ⊕ z. (PEq1) π 1 (x||y) = Eg x. (PEq2) π 2 (x||y) = Eg y.
|| is intended to model concatenation, ⊕ is the classical XOR and π j are the projections. Next rules are consequences of the closure rules from Section 4.

(SyE) If φ 1 ∼ = φ 2 then φ 2 ∼ = φ 1 . (TrE) If φ 1 ∼ = φ 2 and φ 2 ∼ = φ 3 then φ 1 ∼ = φ 3 . (XE1) If r ∈ (f n(σ) ∪ f n(T )) then ν n.r.{σ, x = r ⊕ T } ∼ = ν n.r.{σ, x = r}. (CD1) If (φ |= T 1 ∨ φ |= T 2 ) then φ |= T 1 ||T 2 . (HD1) If ν n.σ |= T and h(T ) ∈ st(σ) then ν n.{σ, x = h(T )} |= T . (XD1) If ν n.σ |= T and r ∈ ( n ∪ f n(T )) then ν n.r.{σ, x = r ⊕ T } |= T .

Trapdoor one-way functions in the symbolic model

We extend the above algebra in order to model trapdoor one-way functions. We add a sort iData and new symbols f : Data × Data → iData ,f -1 : iData × Data → Data, pub : Data → Data. f is a trapdoor permutation, with f -1 being the inverse function. We extend the equational theory:

(OEq1) f -1 (f (x, pub(y)), y) = Eg x.
To simplify the notations, we will use f k (•) instead of f (•, pub(k)). Now we want to capture the one wayness of function f . Computationally, a one-way function only ensures the weakly secrecy of a random argument r (as long as the key k is not disclosed to the adversary). Hence we define S i = ∅ and

S d = {(νk.r.{x k = pub(k), x = f k (r)}, r)}.
The following frame encodes the encryption scheme proposed by Bellare and Rogaway in [START_REF] Bellare | Random oracles are practical: a paradigm for designing efficient protocols[END_REF]:

φ br (m) = νk.r.{x k = pub(k), x a = f k (r), y = g(r) ⊕ m, z = h(m||r)}
where m is the plaintext to be encrypted, f is a trapdoor one-way function, and g and h are hash functions (hence oracles in the ROM model). Now we can see the necessity of p-variables in order to encode IND-CPA security of an encryption scheme. Proving that it holds for any two messages m 1 and m 2 νk.r.

TrE HE1 CD1 GD5 HD1 GD5 OD1 {σ2} |= r {σ2, y = s ′ } |= r {σ2, y = g(r)} |= r {σ2, y = g(r) ⊕ p(x k ), z = t} |= r {σ2, y = g(r) ⊕ p(x k ), z = t} |= p(x k )||r {σ2, y = g(r) ⊕ p(x k ), z = h(p(x k )||r)} ∼ = {σ2, y = g(r) ⊕ p(x k ), z = t} (T 1) {x k = pub(k), xa = f k (r), y = g(r) ⊕ p(x k ), z = h(p(x k )||r)} ∼ = {x k = pub(k), xa = f k (r), y = s, z = t}

GE1

TrE GE1 HE1 GD5 OD1 {σ2} |= r {σ2, y = s} |= r {σ2, y = g(r)} ∼ = {σ2, y = s} {σ2, y = g(r) ⊕ p(x k )} ∼ = {σ2, y = s ⊕ p(x k )} XE1 {σ2, y = s ⊕ p(x k )} ∼ = {σ2, y = s} {σ2, y = g(r) ⊕ p(x k )} ∼ = {σ2, y = s} {σ2, y = g(r) ⊕ p(x k ), z = t} ∼ = {σ2, y = s, z = t}
{x k = pub(k), x a = f k (r), y = g(r) ⊕ m 1 , z = h(m 1 ||r)} ∼ = νk.r.{x k = pub(k), x a = f k (r), y = g(r) ⊕ m 2 , z = h(m 2 ||r)}
is not enough. We did not capture that the adversary is adaptive and she can choose her challenges depending on the public key. Hence we must prove a more stronger equivalence, namely that it holds for any terms p(x k ) and p ′ (x k )

νk.r.{x k = pub(k), x a = f k (r), y = g(r) ⊕ p(x k ), z = h(p(x k )||r)} ∼ = νk.r.{x k = pub(k), x a = f k (r), y = g(r) ⊕ p ′ (x k ), z = h(p ′ (x k )||r)}
The reader noticed that for asymmetric encryption, this suffices to ensure IND-CPA: possessing the public key and having access to hash-oracles, suffices to encrypt any message, hence it is not necessary to have an oracle to encrypt messages.

Actually, in our case it suffices to prove νk.r.

{x k = pub(k), x a = f k (r), y = g(r) ⊕ p(x k ), z = h(p(x k )||r)} ∼ = νk.r.s.t.{x k = pub(k), x a = f k (r), y = s, z = t}.
By transitivity, this implies: for any two challenges that adversary chooses for p(x k ), the distributions she gets are indistinguishable.

Before proceeding with the proof, we first state some rules that are consequences of the definition of S d and of the closure rules from Section 4.

(OD1) If f is a one-way function, then νk.r.{x k = pub(k), x = f k (r)} |= r. (ODg1) If f is a one-way function and ν n.νk.{x k = pub(k), x = T } ∼ = νr.νk.{x k = pub(k), x = r}, then ν n.νk.{x k = pub(k), x = f k (T )} |= T .
The proof of IND-CPA security of Bellare-Rogaway scheme is presented in Figure 1. To simplify the notations we suppose that all names in frames are restricted and we note σ 2 ≡ x k = pub(k), x a = f k (r).

Partially one-way functions in the symbolic model

In this subsection, we show how we can deal with trapdoor partially one-way functions. This extension is motivated by Pointcheval's construction in [START_REF] Hasan | Chosen-ciphertext security for any one-way cryptosystem[END_REF]. In contrast to the previous subsection, we demand for function f a stronger property than one-wayness. Let Data 1 be a new sort, and let f : Data 1 × Data × Data → iData be a function and let f

-1 : iData × Data → Data 1 , such that (OEq1) f (f -1 (x, y), z, pub(y)) = Eg x.
The function f is said partially one way, if for any given f (s, r, pub(k)), it is impossible to compute in polynomial time a corresponding s without the trapdoor k. In order to deal with the fact that f is now partially one-way, we define

S i = ∅ and S d = {(νk.r.s.{x k = pub(k), x = f k (r, s)}, r)}.
The following frame encodes the encryption scheme proposed by Pointcheval in [START_REF] Hasan | Chosen-ciphertext security for any one-way cryptosystem[END_REF].

φ po (m) = νk.r.s.{x k = pub(k), x a = f k (r, h(m||s)), y = g(r) ⊕ (m||s)}
where m is the plaintext to be encrypted, f is a trapdoor partially one-way function, and g and h are hash functions. To prove IND-CPA security of this scheme, we can show in our framework that νk.r.s. Before proceeding with the proof we first state the next rule that is a consequence of the definition of

{x k = pub(k), x a = f k (r, h(p(x k )||s)), y = g(r) ⊕ (p(x k )||s)} ∼ = νk.r.s 1 .s 2 .{x k = pub(k), x a = f k (r, s 1 ), y = s 2 }. TrE HE1 GD6 SyE XE1 {σ2, x = r, y = s2 ⊕ (p(x k )||s)} ∼ = {σ2, x = r, y = s2} {σ2, y = s2, x = r} ∼ = {σ2, y = s2 ⊕ (p(x k )||s), x = r} GD5 ODp1 {σ2} |= r {σ2, y = s2} |= r {σ2, y = s2 ⊕ (p(x k )||s)} |= r {σ2, y = g(r) ⊕ (p(x k )||s)} ∼ = {σ2, y = s2 ⊕ (p(x k )||s)} (T 2) {x k = pub(k), xa = f k (r, h(p(x k )||s)), y = g(r) ⊕ (p(x k )||s)} ∼ = {x k = pub(k), xa = f k (r, s1), y = s2}
TrE XE1 {σ2, y = s2 ⊕ (p(x k )||s)} ∼ = {σ2, y = s2} GE1 HE1 CD1 GD5 GD1 ∅ |= s {x k = pub(k), xa = f k (r, s1)} |= s {x k = pub(k), xa = f k (r, s1)} |= p(x k )||s {σ2} ∼ = {x k = pub(k), xa = f k (r, s1)} {σ2, y = s2} ∼ = {x k = pub(k), xa = f k (r, s1), y = s2} {σ2, y = s2 ⊕ (p(x k )||s)} ∼ = {x k = pub(k), xa = f k (r, s1), y = s2}
S d . (ODp1) If f is an one-way function, then νk.r.s.{x k = pub(k), x = f k (r, s)} |= r.
The proof of IND-CPA security of Pointcheval scheme is presented in Figure 3. To simplify notations we suppose that all names in frames are restricted and we note

σ 2 ≡ x k = pub(k), x a = f k (r, h(p(x k )||s)).

Computational Diffie Hellman Assumption

In this subsection we prove indistinguishability under chosen plaintext attacks of a variant of Hash-ElGamal encryption scheme ( [START_REF] Shoup | Sequences of games: a tool for taming complexity in security proofs[END_REF]) in the random oracle model under the CDH assumption. The proof of the original scheme( [START_REF] Baek | Secure length-saving elgamal encryption under the computational diffie-hellman assumption[END_REF]) can be easily obtained from our proof and it can be done entirely in our framework.

We will consider two sorts G and A, symbol functions exp :

G × A → G, * : A × A → A, 0 A : A, 1 A : A, 1 G : G.
To simplify the notation we write M N instead of exp(M, N ). We extend the equational theory E g by the following equations:

(XEqe1) (x y ) z = Eg x y * z . (XEqe2) x 1 A = Eg x. (XEqe3) x 0 A = Eg 1 G .
To capture the Computational Diffie Hellman Assumption in the symbolic model we define S i = ∅ and S d = {(νg.r.s.{x g = g, x = g s , y = g r }, g s * r )}.

So we have the next rule that is a consequence of the definition of S d . (CDH) νg.r.s.{x g = g, x = g s , y = g r } |= g s * r .

The following frame encodes the Hash-ElGamal encryption scheme. φ hel (m) = νg.r.s.{x g = g, x = g s , y = g r , z = h(g s * r ) ⊕ m} where m is the plaintext to be encrypted, (g, g s ) is the public key and h is a hash function.

The proof of IND-CPA security of Hash-ElGamal's scheme is provided in Figure 5. To simplify the notations we suppose that all names are restricted and we note σ e ≡ x g = g, x = g s , y = g r . In this section we adapt the definition of deductibility and static equivalence ( [START_REF] Baudet | Computationally sound implementations of equational theories against passive adversaries[END_REF]) to our framework. After, we justify why they are too coarse to be appropriate abstractions for indistinguishability and weak secrecy. We also prove that in general they are coarser approximations of indistinguishability and weak secrecy than FIR and FNDR. If φ is a frame, and M, N are terms, then we write (M = E N )φ for M φ = E N φ.

TrE GE1 HE1 GD5 CDH {σe} |= g s * r {σe, z = t} |= g s * r {σe, z = h(g s * r )} ∼ = {σe, z = t} {σe, z = h(g s * r ) ⊕ p(x, xg)} ∼ = {σe, z = t ⊕ p(x, xg)} XE1 {σe, z = t ⊕ p(x, xg)} ∼ = {σe, z = t} {xg = g, x = g s , y = g r , z = h(g s * r ) ⊕ p(x, xg)} ∼ = {xg = g, x = g s , y = g r , z = t}

Definition 8 (Deductibility). A (closed) term

T is deductible from a frame φ where (p i ) i∈I = pvar(φ), written φ ⊢ T , if and only if there exists a term M and a set of terms

(M i ) i∈I , such that var(M ) ⊆ dom(φ),ar(M i ) = ar(p i ), f n(M, M i ) ∩ n(φ) = ∅ and (M = E T )(φ[(M i (T i 1 , . . . , T i k )/p i (T i 1 , . . . , T i k )) i∈I ]
). We denote by ⊢ the logical negation of ⊢.

For instance, we consider the equational theory E g and the frame φ = νk 1 .k 2 .s 1 .s 2 .{x

1 = k 1 , x 2 = k 2 , x 3 = h((s 1 ⊕ k 1 ) ⊕ p(x 1 , x 2 )), x 4 = h((s 2 ⊕ k 2 ) ⊕ p(x 1 , x 2 ))}. Then h(s 1 ) ⊕ k 2 is deductible from φ since h(s 1 ) ⊕ k 2 = Eg x 3 [x 1 /p(x 1 , x 2 )] ⊕ x 2 but h(s 1 ) ⊕ h(s 2 ) is not deductible.
If we consider the frame φ ′ = νk.r.s.{x k = pub(k), x = f k (r||s)} where f is a trapdoor one-way function, then neither r||s, nor r is deductible from φ ′ . So, the one-wayness of f is modelled by the impossibility of inverting f if k is not disclosed. While this is fair for r||s according to the computational guarantees of f , it seems too strong of assuming that r alone cannot be computed if f is "just" one-way. This raises some doubts about the fairness of ⊢ as a good abstraction of weak secrecy. We can try to correct this and add an equation of the form g(f (x||z, pub(y)), y) = Eg x. And now, what about r 1 , if one gives f ((r 1 ||r 2 )||s)? In the symbolic setting r 1 is not deductible; in the computational one we have no guarantee; hence, when one stops to add equations? Moreover, in this way we could exclude "good" one-way functions: in the computational setting, if f is a one-way function, then f ′ (x||y) def = x||f (y), is another one-way function. The advantage of defining non-deductibility as we did it in the Section 4, is that first, we capture "just" what is supposed to be true in the computational setting, and second, if we add more equations to our abstract algebra (because we discovered that the implementation satisfies more equations) in a coherent manner with respect to the initial computational assumptions, then our proofs still remain computationally sound. This is not true for ⊢.

Definition 9 (Test).

A test for a frame φ is a triplet ((M i ) i∈I , M, N ) such that var(M, N ) ⊆ dom(φ),ar

(M i ) = ar(p i ), f n(M, N, M i ) ∩ n(φ) = ∅. Then φ passes the test ((M i ) i∈I , M, N ) if and only if (M = E N )(φ[(M i (T i 1 , . . . , T i k )/p i (T i 1 , . . . , T i k )) i∈I ]).
Definition 10 (Statically Equivalent). Two frames φ 1 and φ 2 are statically equivalent, written as φ 1 ≈ E φ 2 , if and only if (i) dom(σ 1 ) = dom(σ 2 ); (ii) for any test ((M i ) i∈I , M, N ), φ 1 passes the test ((M i ) i∈I , M, N ) if and only if φ 2 passes the test ((M i ) i∈I , M, N ).

For instance, the two frames φ 1 = νk.s.{x 1 = k, x 2 = h(s) ⊕ (k ⊕ p(x 1 ))} and φ 2 = νk.s.{x 1 = k, x 2 = s ⊕ (k ⊕ p(x 1 ))} are statically equivalent with respect to E g . However the two frames

φ ′ 1 = νk.s.{x 1 = k, x 2 = h(s) ⊕ (k ⊕ p(x 1 )), x 3 = h(s)} and φ ′ 2 = νk.s.{x 1 = k, x 2 = s ⊕ (k ⊕ p(x 1 )), x 3 = h(s)} are not. The frame φ ′
2 passes the test ((x 1 ), x 2 , x 3 ), but φ ′ 1 does not. Let us now consider the equational theory from subsection 5.2. Then the following frames νg.a.b.{x 1 = g, x 2 = g a , x 3 = g b , x 4 = g a * b ) and νg.a.b.c.{x 1 = g, x 2 = g a , x 3 = g b , x 4 = g c ) are statically equivalent. This seems right, it is the Decisional Diffie-Hellman assumption. So, a computational implementation that satisfies indistinguishability for the interpretations of this two frames will simply satisfy the DDH assumption. But soundness would imply much more. Even νg.a.b.{x 1 = g, x 2 = g a , x 3 = g b , x 4 = g a 2 * b 2 ) and νg.a.b.c.{x 1 = g, x 2 = g a , x 3 = g b , x 4 = g c ) will be statically equivalent. It is unreasonable to assume that this is true for the computational setting. And as for non-deductibility, the advantage of considering FIR as the abstraction of indistinguishability, is that if we are adding equations in a coherent manner with respect to the initial computational assumptions (that is with S i ), then our proofs still remain computationally sound.

Next proposition says that if the initial sets S d and S i are reasonable, then the obtained FIR and FNDR are finer approximations of indistinguishability and weak secrecy than ⊢ and ≈ E .

Conclusion

In this paper we developed a general framework for relating formal and computational models for generic encryption schemes in the random oracle model. We proposed general definitions of formal indistinguishability relation and formal non-derivability relation, that is symbolic relations that are computationally sound by construction. We extended previous work with respect to several aspects. First, our framework can cope with adaptive adversaries. This is mandatory in order to prove IND-CPA security. Second, many general constructions use oneway functions, and often they are analyzed in the random oracle model: hence the necessity to capture the weak secrecy in the computational world. Third, the closure rules we propose are designed with the objective of minimizing the initial relations which depend of the cryptographic primitives and assumptions. We illustrated our framework on the generic encryption scheme proposed by Bellare and Rogaway [START_REF] Bellare | Random oracles are practical: a paradigm for designing efficient protocols[END_REF] and on Hash El Gamal [START_REF] Baek | Secure length-saving elgamal encryption under the computational diffie-hellman assumption[END_REF].

As future works, we project to study the (relative) completeness of various equational symbolic theories. Another ambitious extension will be to capture fully active adversaries.

M ) = Pr[ φ, ê r ← [[φ, M ]] B : B O ( φ) = ê] = Pr[ φ′′ , ê r ← [[φ ′ φ, M ]] A : A O ( φ′′ ) = ê] = Adv(A, η, φ ′ φ |= M ).
In addition, the execution time of B is a polynomial w.r.t. to η and the execution time of A, using that the size of encoding of φ ′ is constant in η.

⊓ ⊔ Let us suppose that there exists a probabilistic polynomial-time adversary B such that (

[[φφ 1 ]] B ) ≈ ([[φφ 1 ]] B ), that is Pr[ φ′ r ← [[φφ 1 ]] B : B O ( φ′ ) = 1] -Pr[ φ′ r ← [[φφ 2 ]] B : B O ( φ′ ) = 1]
is non-negligible.

Then we construct an adversary

A such that Pr[ φ r ← [[φ 1 ]] A : A O ( φ) = 1] -Pr[ φ r ← [[φ 2 ]] A : A O ( φ) = 1] is non-negligible.
The adversary A uses B as a black box to first get φ r ← [[φ i ]] B ; then it interprets all variables in var(φ) by bitstrings obtained in the previous stage (as var(φ) ⊆ dom(φ i )); then it continues to use B as a black box in order to interpret all queries from pvar(φ); finally it get a concrete frame from [[φφ i ]] B and passes it to B; it answers as B. Hence, the advantage of A equals the advantage of B, which is non-negligible. In addition, A runs in probabilistic polynomial-time since B runs in probabilistic polynomial-time and the size of encoding of φ is constant in η. This is a contradiction with φ 1 ∼ = φ 2 being ≈-sound. Hence φφ 1 ∼ = φφ 2 is also ≈-sound.

⊓ ⊔ (GE2) φ ∼ = φ ′ for any frame φ ′ such that φ ′ = E φ.

Proof. Obviously, using the =-soundness of = E . ⊓ ⊔ (GE3) τ (φ) ∼ = φ for any renaming τ . g -1 (ĝ(bs)) = bs] is negligible. Then, the correctness of rule (GE4) is easy to prove using the =-soundness of = E and noticing that the context N can be used to build the inverse function of λr.M (r).

Let us suppose that Pr[bs r ← [[s]] : g -1 (ĝ(bs)) = bs] is negligible. To easy notations, we note S = [[s]], S 1 = {bs ∈ S| g -1 (ĝ(bs)) = bs}, S 2 = {bs ∈ S| g -1 (ĝ(bs)) = bs}, s = |S|, s i = |S i |. Our hypothesis is equivalent to s 2 = s * η for some negligible function η. Also, it easy to see that ĝ : S 1 → ĝ(S 1 ) is an injective function, and hence a bijective function too. So, if bs ′ ∈ ĝ(S 1 ) we know that there is exactly one element in S 1 noted i(bs ′ ) such that ĝ(i(bs ′ )) = bs ′ . We note in this case S Proof. In the random oracle model, hash functions are drawn uniformly at random from the space of functions of suitable type at the beginning of the interpretation of the frame. Thus, the images that the hash function associates to different inputs are completely independent. Therefore, one can delay the draw of each hash value until needed. We use σ Proof. Obviously, using that indistinguishability is an equivalence relation.

⊓ ⊔

  {σ 1 , x = T [M/z]} ∼ = ν n.{σ 2 , x = T [N/z]} and ν n.σ 1 |= M then ν n.σ 2 |= N . And now the rule that captures the power of hash functions in the Random Oracle Model: the image by a random function of a weakly secret value is a completely random value. (HE1) If ν n.r.σ[r/h(T )] |= T and r ∈ n(σ), then ν n.σ ∼ = ν n.r.σ[r/h(T )].

Fig. 1 .

 1 Fig. 1. Proof of IND-CPA security of Bellare-Rogaway scheme.

Fig. 2 .

 2 Fig. 2. Tree (T 1) from Figure 1.

Fig. 3 .

 3 Fig. 3. Proof of IND-CPA security of Pointcheval scheme.

Fig. 4 .

 4 Fig. 4. Tree (T 2) from Figure 3.

Fig. 5 .

 5 Fig. 5. Proof of IND-CPA security of Hash-ElGamal's scheme

Proposition 1 .

 1 Let (S d , S i ) be such that S d ⊆ ⊢ and S i ⊆≈ E . Then S d |= ⊆ ⊢ and S i ∼ = ⊆≈ E .

( 1 |S|

 1 GD1) νr.∅ |= r. Proof. To easy notations, we note S = [[s]]. Then we have Pr[bs r ← [[s]] : A() = bs] = bs∈S Pr[bs ′ r ← [[s]] : bs ′ = bs] * Pr[A() = bs] Now we use the assumption that all sorts are suppposed to be of size exponential in η. ⊓ ⊔ (GD2) If φ |= M then τ (φ) |= τ (M ) for any renaming τ .Proof. Using the fact that renamings do not change distributions, we get[[τ (φ), τ (M )]] = [[φ, M ]]. ⊓ ⊔ (GD3) If φ |= M then φ |= N for any term N = E M . (GD4) If φ |= M then φ ′ |= M for any frame φ ′ = E φ.Proof. Obviously, using the =-soundness of = E . ⊓ ⊔(GD5) If φ |= M then φ ′ φ |= M for any frame φ ′ such that var(φ ′ ) ⊆ dom(φ) and n(φ ′ ) ∩ bn(φ) = ∅.Proof. Let φ ′ such that var(φ ′ ) ⊆ dom(φ) and n(φ ′ ) ∩ bn(φ) = ∅. Let us suppose that φ |= M is ⊢-sound, and let us prove that φ ′ φ |= M is also ⊢-sound. We have to show that for any probabilistic polynomial-time adversary A against φ ′ φ |= M , there exists an adversary B against φ |= M that satisfies the conditions of Fact A1. The adversary B uses A as a black box to first compute φ r ← [[φ]] A ; then it interprets all variables in var(φ ′ ) by bitstrings obtained in the previous stage (as var(φ ′ ) ⊆ dom(φ)); it continues to use A as a black box in order to interpret all queries from pvar(φ ′ ); finally it gets a concrete frame from [[φ ′ φ]] A and passes it to A; it answers as A. Hence, the advantage of B equals the advantage of A, Adv(B, η, φ |=

  GD6) If T, U are terms such that U [T /y] = E z and z ∈ var(T )\var(U ) and (f n(T )∪f n(U ))∩ n = ∅, then for all substitutions σ 1 , σ 2 such that x ∈ dom(σ i ) and ν n.{σ 1 , x = T [M/z]} ∼ = ν n.{σ 2 , x = T [N/z]} and ν n.σ 1 |= M then ν n.σ 2 |= N . Proof. Let us suppose that ν n.σ 1 |= M is ⊢-sound and ν n.{σ 1 , x = T [M/z]} ∼ = ν n.{σ 2 , x = T [N/z]} is ≈-sound,and let us prove that ν n.σ 2 |= N is also ⊢-sound.We have to show that for any probabilistic polynomial-time adversary A against ν n.σ 2 |= N , there exists adversaries B 1 against ν n.{σ 1 , x = T [M/z]} ∼ = ν n.{σ 2 , x = T [N/z]}, and B 2 against ν n.σ 1 |= M which satisfy the conditions of Fact A1.

Proof.

  Using the fact that renamings do not change distributions, we get [[τ (φ)]] = [[φ]]. ⊓ ⊔ (GE4) If M, N are terms of the same sort such that N [M/z] = E y and y ∈ var(M ) \ var(N ), then for any substitution σ such that r ∈ (f n(σ) ∪ f n(M ) ∪ f n(N )) and x ∈ dom(σ) it holds ν n.r.{σ, x = M [r/y])} ∼ = ν n.r.{σ, x = r}. Proof. We prove that the statistical distance d([bs r ← [[s]] : ĝ(bs)], [bs r ← [[s]] : bs]) is negligible for any computational functions ĝ : [[s]] → [[s]] and g -1 : [[s]] → [[s]] such that Pr[bs r ← [[s]] :

=bs ′ ∈S 1 2 χ

 12 1,bs ′ = S 1 \ {i(bs ′ )}. Moreover, |S \ ĝ(S 1 )| = |S \ S 1 | = s 2 . d([bs r ← [[s]] : ĝ(bs)], [bs r ← [[s]] : bs]) = bs ′ ∈S Pr[bs r ← [[s]] : ĝ(bs) = bs ′ ] -1 s Pr[bs r ← [[s]] : ĝ(bs) = bs ′ ] -1 s + bs ′ ∈S 2 Pr[bs r ← [[s]] : ĝ(bs) = bs ′ ] -1 s ≤ bs ′ ∈S 1 ∩ĝ(S 1 ) Pr[bs r ← [[s]] : ĝ(bs) = bs ′ ] -1 s + bs ′ ∈S 1 ∩(S\ĝ(S 1 )) Pr[bs r ← [[s]] : ĝ(bs) = bs ′ ] -1 s + η ≤ bs ′ ∈S 1 ∩ĝ(S 1 ) 1 s * bs∈S χ [ĝ(bs)=bs ′ ] -1 s + η + η = bs ′ ∈S 1 ∩ĝ(S 1 ) 1 s * χ [ĝ(i(bs ′ )))=bs ′ ] + bs∈S 1,bs ′ χ [ĝ(bs)=bs ′ ] + bs∈S [ĝ(bs)=bs ′ ] -1 + 2 * η ≤ bs ′ ∈S 1 ∩ĝ(S 1 ) 1 s * 1 + 0 + s 2 -1 + 2 * η = 3 * η ⊓ ⊔(HE1) If ν n.r.σ[r/h(T )] |= T and r ∈ n(σ), then ν n.σ ∼ = ν n.r.σ[r/h(T )].

  [•] for σ[•/h(T )], i.e. σ where all occurrences of h(T ) are replaced by •. Now, using that ν n.r.σ[r/h(T )] |= T we get[[ν n.σ[h(T )/•]}]] A = H r ← Ω; O = H; ( φ[•], bs) r ← [[(ν n.σ[•], T )]] H,A : φ[H(bs)/•] (since ν n.r.σ[r/h(T )] |= T one can delay the draw of h([[T ]])) ∼ H r ← Ω; O = H; ( φ[•], bs) r ← [[(ν n.σ[•], T )]] H,A ; v r ← [[s(T )]]; O = H[H → H[bs → v]] : ( φ[v/•]) (since ν n.r.σ[r/h(T )] |= T the probability that A query h([[T ]]) is negligible) ∼ H r ← Ω; O = H; ( φ[•], bs) r ← [[(ν n.σ[•], T )]] H,A ; v r ← [[s(T )]] : ( φ[v/•]) = H r ← Ω; O = H; φ[•] r ← [[ν n.σ[•]]] H,A ; v r ← [[s(T )]] : ( φ[v/•]) = [[ν n.νr.{σ[r/•]}]] A ⊓ ⊔ (SyE) If φ 1 ∼ = φ 2 then φ 2 ∼ = φ 1 . (TrE) If φ 1 ∼ = φ 2 and φ 2 ∼ = φ 3 then φ 1 ∼ = φ 3 .

  a name or a variable, and st(l(T 1 , . . . , T k ))def = {l(T 1 , . . . , T k )} i∈{1,...k} st(T i ), if l ∈ F ∪ H ∪ P. Aterm T is closed if and only if it does not have any free variables (but it may contain p-variables, names and constant symbols), that means var(T ) = ∅. The set of terms is denoted by T. Symbols in F are intended to model cryptographic primitives, symbols in H are intended to model cryptographic oracles (in particular, hash functions in the ROM model), whereas names in N are used to model secrets, that is, concretely random numbers. Variables p ∈ P are intended to model queries and challenges made by adversaries (they can depend on previous queries).

This work has been partially supported by the ANR projects SCALP, AVOTE and SFINCS

A Proofs

Actually, it is easy to see easy that ( S d |= , S i ∼ = ) is the least fixed point of some continuous function

GD6),(GE1),...,(GE4), (HE1), symmetry and transitivity. It can be constructed by applying iteratively (

, with n ∈ AE until reaching a fixpoint.

Now we prove that

Most of the closure rules have premises that assume some hypothesis on |= or ∼ =. Let suppose that for any such closure rule (R), we prove its computational soundness, that is, the following fact: Fact A1 For any adversary A against the conclusion of the rule (R), there exists some adversary B (or tuple of adversaries B i ) breaking one of the premises of (R) , and moreover:

1. the advantage of A is a polynomial w.r.t. to η and the advantage of B (advantages of B i , respectively) and 2. the adversary A has an execution time which is a polynomial w.r.t. to η and the execution time of B (execution times of B i , respectively). Now let suppose that there is some element (e 1 , e 2 ) in S d |= or S i ∼ = which is not ⊢-sound or ≈-sound. Let n be the number of steps needed to include (e 1 , e 2 ) in S d |= or S i ∼ = , i.e. the minimal number of iterations ( S d n , S i n ) needed to get (e 1 , e 2 ) ∈ S d n or (e 1 , e 2 ) ∈ S i n .

Then, for any adversary A 0 against the soundness of (e 1 , e 2 ), we can construct an adversary A n against the soundness of an element (e 0 1 , e 0 2 ) of S d or S i , such that 1. the advantage of A 0 is bounded by an expression which depends of n and which is a polynomial w.r.t. η and the advantage of A n , and 2. the execution time of A n is bounded by an expression which depends of n and which is a polynomial w.r.t. η and the execution time of A 0 .

Since our reasoning is asymptotically (and n is independent from η), this would imply that (e 0 1 , e 0 2 ) is not sound, contradiction with the ⊢-soundness of S d or the ≈-soundness of S i . In what follows we prove soundness for all rules of section 4.

In our case we will provide an adversary B to play the role of B 1 and we will use the adversary A as player for the role of B 2 , too.

Since f n(T ) ∩ n = ∅, it follows that T (z) is constructible using only dom(σ i ). Hence, the adversary B uses A as a black box to first get either ( φ,

Then A stops and answers some string bs. If t(ê) = t(bs), B answers 1 and stops. If t(ê) = t(bs), B picks randomly a bit c, answers c and stops. From the definition of B, and using the = E injectivity of T and the =-soundness of = E , we have the following:

where n 1 (η) and n 2 (η) are some negligible functions.

Now we have

for some well-chosen negligible function n 3 (η). Moreover, it is easy to see that the execution time of B is a polynomial w.r.t. to η and the execution time of A, using that the test t(ê) ? = t(bs), and picking uniformly a random bit can be done in a time polynomial w.r.t. to η.

⊓ ⊔

Proof. Let φ such that var(φ) ⊆ dom(φ i ) and n(φ) ∩ bn(φ i ) = φ. Let us suppose that φ 1 ∼ = φ 2 is ≈-sound, and let us prove that φφ 1 ∼ = φφ 2 is also ≈-sound. We have to show that for any probabilistic polynomial-time adversary B, ([ Proof. Consequence of rules (OD1), (GE1) and (GD6). ⊓ ⊔