M Bornert

P P O N T E Casta

Keywords: rate-dependent plasticity, self-consistent estimates, heterogeneous materials, creep of polycrystals, second-order theory, nonlinear homogenization

The 'second-order' homogenization procedure of Ponte Castañeda is used to propose new estimates of the self-consistent type for the effective behaviour of viscoplastic polycrystals. This is accomplished by means of appropriately generated estimates of the self-consistent type for the relevant 'linear thermoelastic comparison composite', in the homogenization procedure. The resulting nonlinear self-consistent estimates are the only estimates of their type to be exact to second order in the heterogeneity contrast, which, for polycrystals, is determined by the grain anisotropy. In addition, they satisfy the recent bounds of Kohn & Little for two-dimensional power-law polycrystals, which are known to be significantly sharper than the Taylor bound at large grain anisotropy. These two features combined, suggest that the new self-consistent estimates, obtained from the second-order procedure, may be the most accurate to date. Direct comparison with other self-consistent estimates, including the classical incremental and secant estimates, for the special case of power-law creep, appear to corroborate this observation.

Second-order estimates of the self-consistent type for viscoplastic polycrystals

Introduction

In spite of being a classical problem [START_REF] Taylor | Plastic strains in metals[END_REF], the theoretical prediction of the effective response of plastic and viscoplastic polycrystals is still very much open. This is because the so-called 'classical' methods have been found to tend to overestimate the effective response, especially at large heterogeneity and nonlinearity (see, for example, [START_REF] Gilormini | A shortcoming of the classical nonlinear extension of the self-consistent model[END_REF] for the analogous problem of two-phase nonlinear composites). This paper is concerned with the application of a recently developed nonlinear homogenization method [START_REF] Ponte Castañeda | Exact second-order estimates for the effective mechanical properties of nonlinear composite materials[END_REF], to estimate the effective flow stress of viscoplastic polycrystals. The method requires the computation of the effective response of a fictitious 'linear thermoelastic comparison polycrystal' as an intermediate step, which is accomplished by means of the self-consistent estimates of [START_REF] Laws | On the thermostatics of composite materials[END_REF] and [START_REF] Willis | Variational and related methods for the overall properties of composites[END_REF].

The resulting self-consistent estimates for the nonlinear viscoplastic polycrystals have the unique property of being exact to second order in the heterogeneity contrast. In other words, they agree to second order exactly in a suitable measure of the heterogeneity, which in the case of polycrystals is related to the grain anisotropy, with the asymptotic results of [START_REF] Suquet | Small-contrast perturbation expansions for the effective properties of nonlinear composites[END_REF] for weakly heterogeneous systems. They are, in fact, the first estimates of the self-consistent type for nonlinear polycrystals to have this property, which is widely known to hold for the corresponding linear-elastic estimates. In addition, the new self-consistent estimates will be shown to satisfy a recently established bound [START_REF] Kohn | Some model problems of polycrystal plasticity with deficient basic crystals[END_REF], for a certain class of model two-dimensional polycrystals, which is known to be significantly more restrictive than the corresponding Taylor and Hashin-Shtrikman bounds at large grain anisotropy [START_REF] Dendievel | Bounds for the creep behavior of polycrystalline materials[END_REF][START_REF] Debotton | Variational estimates for the creep behavior of polycrystals[END_REF]. In fact, the Kohn-Little bound scales with the square root of the grain-anisotropy parameter, whereas the Taylor and Hashin-Shtrikman bounds scale linearly with this parameter. These two properties combined-that they are exact for small grain anisotropy and that they satisfy the Kohn-Little bound at large grain anisotropystrongly suggest that these new self-consistent estimates may be the most accurate to date. That this may indeed be the case will be argued by direct comparison with the classical 'incremental' and 'secant' methods of [START_REF] Hill | Continuum micro-mechanics of elastoplastic polycrystals[END_REF] see also [START_REF] Hutchinson | Bounds and self-consistent estimates for creep of polycrystalline materials[END_REF] and [START_REF] Berveiller | An extension of the self-consistent scheme to plastically-flowing polycrystals[END_REF], respectively, as well as with other more recent methods including the 'tangent' method of [START_REF] Molinari | A self-consistent approach of the large deformation polycrystal viscoplasticity[END_REF] and the related 'affine' method proposed by [START_REF] Zaoui | Modeling stress-dependent transformation strains of heterogeneous materials[END_REF] and independently by P. Suquet (1996, personal communication). Comparisons will also be carried out with the variational self-consistent estimates of Ponte Castañeda & Nebozhyn (1997), which have already been found to satisfy both the Taylor and Kohn-Little bounds.

Effective behaviour of viscoplastic polycrystals

A polycrystal is an aggregate of a large number of perfectly bonded single-crystal grains with varying orientations. It is assumed to occupy a region in space, Ω, and can be thought of as an N -phase heterogeneous material, where each phase is defined as the subregion Ω (r) (r = 1, . . . , N) occupied by all grains of a given orientation, as defined by a rotation tensor, Q (r) , relative to a reference crystal with known orientation. Each grain is assumed to undergo viscoplastic deformation on a set of K preferred crystallographic slip systems. These are defined by the second-order tensors

μ (r) (k) = 1 2 (n (r) (k) ⊗ m (r) (k) + m (r) (k) ⊗ n (r) (k) )
, where the unit vectors n (r) (k) and m (r) (k) denote the normal to the slip plane and the slip direction in the kth (k = 1, . . . , K) system, respectively, for each grain orientation r (r = 1, . . . , N). The symbol ⊗ denotes the dyadic product. Note that (r) , where the μ (k) define the slip systems of the reference crystal.

μ (r) (k) = Q (r)T μ (k) Q
The resolved shear stress on the kth slip systems of grains with orientation r is defined by

τ (r) (k) = σ • μ (r) (k) ,
(2.1) so that, neglecting elastic effects, the strain rate, ε, and the stress, σ, in these grains are related by

ε = ∂u (r) ∂σ , u (r) (σ) = K k=1 φ (k) (τ (r) (k) ), (2.2)
where u (r) is the stress potential of the crystals with orientation r, defined in terms of the slip potentials φ (k) , typically assumed to be convex. In these relations, the dot denotes the inner product of two second-order tensors (e.g.

σ • μ = σ ij μ ij ).
For reasons to be discussed in the following section, it is preferable to work with the dissipation potentials w (r) , which are the Legendre transforms of the stress potentials u (r) , such that

w (r) (ε) = (u (r) ) * (ε) = max σ {σ • ε -u (r) (σ)}.
(2.3)

Of course, ε and σ are related by

σ = ∂w (r) ∂ε , (2.4)
which is the inverse of (2.2).

Given the dissipation potentials w (r) for the various grain orientations, the corresponding dissipation potential for the polycrystal may be written

w(x, ε) = N r=1 χ (r) (x)w (r) (ε), (2.5)
where the characteristic function χ (r) is equal to one if the position vector x is inside a grain with orientation r (i.e. x ∈ Ω (r) ) and zero otherwise. The volume averages, • and • (r) , are defined over the polycrystal (Ω) and over grains with orientation r (Ω (r) ), respectively, so that, for example, the scalars c (r) = χ (r) serve to characterize the crystallographic texture of the polycrystal. Then, assuming that the size of the typical grain is small relative to the size of the specimen under consideration, the effective viscoplastic response of the polycrystal may be written in the form

σ = ∂ W ∂ ε , (2.6)
where

W ( ε) = min ε∈K( ε) w(x, ε) = min ε∈K( ε) N r=1 c (r) w (r) (ε) (r) , (2.7)
is the effective dissipation potential for the polycrystal, σ = σ and ε = ε are the average stress and the average strain rate in the polycrystal, and K is the set of kinematically admissible strains:

K( ε) = {ε | there is v with ε = 1 2 [∇v + (∇v) T ] in Ω, v = εx on ∂Ω}.
(2.8)

Second-order estimates for viscoplastic polycrystals

As already mentioned in § 1, the second-order procedure was proposed by Ponte Castañeda (1996) to generate estimates for the effective behaviour of nonlinear composites that have the distinctive property of being exact to second order in the contrast. This is a particularly useful property for materials such as face-centred cubic polycrystals, which, because of the relatively low degree of anisotropy in the grains, exhibit fairly small levels of heterogeneity. However, as already demonstrated empirically by Ponte Castañeda (1996) for two-phase composites, the second-order procedure also seems to deliver accurate results at high contrast, for example, for rigidly reinforced systems. In this section, an abbreviated derivation of the second-order procedure is given, together with an application to the computation of self-consistent estimates for the class of viscoplastic polycrystals described in § 2.

The basis for the second-order procedure is the first-order Taylor formula (with remainder) for the phase potentials w (r) . Introducing reference strains ε(r) , the Taylor formula for w (r) about ε(r) is given by

w (r) (ε) = w (r) ( ε(r) ) + ρ (r) • (ε -ε(r) ) + 1 2 (ε -ε(r) ) • L (r) (ε -ε(r) ), (3.1)
where ρ (r) and L (r) physically correspond to an internal stress and a tangent modulus tensor, respectively, with components

ρ (r) ij = ∂w (r) ∂ε ij ( ε(r) ) and L (r) ijkl = ∂ 2 w (r) ∂ε ij ∂ε kl (γ (r) ), (3.2)
respectively. Note that L (r) depends on the strain

γ (r) = λ (r) ε(r) + (1 -λ (r) )ε,
where λ (r) depends on ε and is such that 0 < λ (r) < 1. It then follows from equation (2.7)-by making the approximation that the reference strains, γ (r) = γ(r) , are constant in each phase-that the effective potential, W , of the nonlinear composite may be estimated as

W ( ε) ≈ N r=1 c (r) [w (r) ( ε(r) ) -ρ (r) • ε(r) + 1 2 ε(r) • L (r) ε(r) ] + Ψ , (3.3) where Ψ = min ε∈K(ε) 1 2 ε • Lε -l • ε . (3.4)
In this last relation, use has been made of the definitions:

l (r) = L (r) ε(r) -ρ (r) (3.5)
and

l(x) = N r=1 χ (r) (x)l (r) , L(x) = N r=1 χ (r) (x)L (r) . (3.6)
Note that the variational problem Ψ , defined by (3.4), corresponds to a thermoelastic polycrystal, as made evident by the Euler-Lagrange equations:

(L ijkl v k,l -l ij ) ,j = 0 in Ω, v i = εij x j on ∂Ω. (3.7)
It follows that the approximation (3.3) for the effective potential, W , of the nonlinear polycrystal is easier to compute than the corresponding exact expression (2.7), because it requires the solution of a linear problem instead of a nonlinear one. Thus, given an estimate for Ψ , the expression (3.3) provides a corresponding estimate for W , for all choices of the ε(r) and γ(r) . The prescriptions consisting in setting

ε(r) = γ(r) = ε (r) , (3.8)
where ε is the strain in the thermoelastic comparison composite, were proposed by Ponte Castañeda (1996), based on the physical intuition that the strain, ε, in phase r would oscillate about its average, ε(r) , in phase r, in such a way that large deviations would only be expected in regions of relatively small measure. A more rigorous justification for these prescriptions has been given by Ponte Castañeda & [START_REF] Ponte Castañeda | Variational second-order estimates for nonlinear composites[END_REF], who have shown that the resulting second-order estimates can be given a stationary variational interpretation. The prescription (3.8) for the ε(r) , also allows further simplification of the estimate (3.3) for W , as has been shown by Ponte Castañeda & Suquet (1998). In fact, the Hill condition for the thermoelastic comparison composite ensures that:

ε • (Lε -l) = ε • Lε -l , (3.9)
which, using the definition (3.5) for the polarizations l (r) , leads to

Ψ = 1 2 N r=1 c (r) [ρ (r) • ( ε + ε (r) ) + ( ε (r) -ε(r) ) • L (r) ε -ε (r) • L (r) ε(r) ]. (3.10)
This result, combined with the prescription (3.8), can be used to rewrite the estimate (3.3) in the simpler form

W ( ε) = N r=1 c (r) w (r) ( ε(r) ) + 1 2 ∂w (r) ∂ε ( ε(r) ) • ( ε -ε(r) ) , (3.11)
where the ε(r) are determined by the prescriptions (3.8) and the approximate equality has been replaced by an exact equality for convenience.

It is also possible to work analogously with a Taylor expansion of the stress potentials, u (r) , to generate a corresponding estimate for the effective stress potential, Ũ . Unfortunately, the estimate for Ũ is not the Legendre dual of estimate (3.11) for W , and is therefore not equivalent to it. As suggested in Ponte Castañeda (1996), the expansion based on the dissipation potentials is preferred in plasticity, as a consequence of the fact that, for the physical nonlinearity present in plasticity and creep, the Taylor expansions on the dissipation potentials are expected to be more accurate than the corresponding expansions on the stress potentials. More details on this issue will be given in § 4.

Given the simplified form (3.11) for W , the implementation of the second-order procedure now only requires estimates for the phase averages, ε(r) , of the strain field in the variational thermoelastic problem (3.4), or, equivalently, in the boundary-value problem (3.7). Since this problem is linear, the principle of superposition ensures that the phase averages, ε(r) , can be given the form [START_REF] Laws | On the thermostatics of composite materials[END_REF]:

ε(r) = A (r) ε -a (r) ,
(3.12)

where the A (r) and a (r) are the relevant fourth-and second-order localization tensors, respectively. Self-consistent estimates for these tensors have been given by [START_REF] Laws | On the thermostatics of composite materials[END_REF] and [START_REF] Willis | Variational and related methods for the overall properties of composites[END_REF]. They can be written in the forms:

A (r) = [L (r) + L ] -1 P -1 (3.13)
and

a (r) = [L (r) + L ] -1 N s=1 c (s) (A (s)
) T l (s) -l (r) .

(3.14)

In these relations, L = P -1 -L is the constraint tensor defined by [START_REF] Hill | Continuum micro-mechanics of elastoplastic polycrystals[END_REF], where L is the self-consistent estimate for the effective modulus tensor which is obtained as the solution of the implicit equation (3.15) also involving L . It is useful to recall that, while the derivation of [START_REF] Laws | On the thermostatics of composite materials[END_REF] was based on the classical interpretation of the self-consistent method, in terms of the solution of the problem of an inclusion embedded in the effective medium, the more general derivation of [START_REF] Willis | Variational and related methods for the overall properties of composites[END_REF] made use of the Hashin-Shtrikman variational principles allowing a more rigorous (i.e. variational) interpretation of the result in terms of two-point correlation functions. In the first case, the tensor P is associated with the solution of an ellipsoidal inclusion of given shape in an infinite matrix with modulus tensor L. In the second, P depends on the shape of the two-point correlation functions (see [START_REF] Willis | Variational and related methods for the overall properties of composites[END_REF].

[ L + L ] -1 = N s=1 c (s) [L (s) + L ] -1 ,
The second-order estimates (3.11) hold for fairly general classes of viscoplastic polycrystals. In particular, they are able to account for different power-law exponents (or even more general flow rules) for different types of slip systems. In addition, elastic, hardening and texture evolution effects can, and should, be included for realistic modelling of metals (see [START_REF] Asaro | Texture development and strain hardening in rate-dependent polycrystals[END_REF]. However, results will be presented here only for the special case of power-law creep, neglecting elastic, hardening and texture effects, since the objective in this short paper is to compare the second-order estimates with earlier estimates. More realistic applications will be given elsewhere.

Application to model power-law polycrystals

The results of § 3 will be used here to determine the effective behaviour of a special class of polycrystals consisting of columnar orthorhombic grains, such that the grains are cylindrical in shape, and their symmetry axes are all aligned with the x 3 -axis. When such polycrystals are loaded in antiplane strain, only two slip systems can be activated. They are those defined by

μ (1) = 1
2 (e 1 ⊗ e 3 + e 3 ⊗ e 1 ) and μ (2) = 1 2 (e 2 ⊗ e 3 + e 3 ⊗ e 2 ), (4.1)

and the problem becomes two-dimensional, where the stress, σ, and strain rate, ε, are characterized by two-dimensional vectors (with components σ 13 , σ 23 and ε 13 , ε 23 , respectively), and the modulus tensor, L, by two-dimensional, symmetric, secondorder tensors (with 2L 1313 and 2L 2323 for the diagonal entries and 2L 1323 for the off-diagonal entry). In addition, the constitutive behaviour of the constituent grains will be assumed to be of the power-law type (e.g. [START_REF] Hutchinson | Bounds and self-consistent estimates for creep of polycrystalline materials[END_REF]), so that the slip potentials in expression (2.2) will be taken to be of the form

φ (k) (τ ) = (τ 0 ) (k) n + 1 |τ | (τ 0 ) (k) n+1 , (4.2)
where n 1 is the strain-rate sensitivity, and (τ 0 ) (1) and (τ 0 ) (2) denote the flow stresses associated with the two slip systems defined by (4.1). Note that the limit as n tends to ∞ is of special interest, as it corresponds to a rigid ideally plastic polycrystal. A local dissipation potential may then be defined for the grains via relations (2.2), (2.3) and (4.2). Under antiplane strain conditions, it reduces to

w (r) (ε) = n n + 1 [(τ 0 ) (1) |ε 13 | 1+(1/n) + (τ 0 ) (2) |ε 23 | 1+(1/n) ]. (4.3)
It follows, by assuming further that the statistical distribution of the grains in the transverse plane is isotropic both in space and orientation, that the polycrystal will exhibit isotropic properties in the plane. Therefore, under antiplane strain conditions, the effective behaviour of the polycrystal is determined by

W ( ε) = n n + 1 τ0 (γ e ) 1+(1/n) , (4.4)
where γe = [ε 2 13 + ε2 23 ] 1/2 and τ0 is the effective flow stress of the polycrystal. The second-order estimates of the self-consistent type are obtained from expression (3.11), where the phase-average strains are obtained by solving equations (3.12)-(3.15) simultaneously for the ε(r) . It is emphasized that the variables L (r) and l (r) , as defined by (3.2) and (3.5), respectively, are dependent on ε(r) , and therefore the above-mentioned set of equations are implicit on the ε(r) and are solved by iteration. Note that L is defined by relation (3.15), which is also implicit in L and must be solved by iteration. Noting that the two-point correlation functions for the distribution of the grain orientations within the polycrystal have been assumed to be isotropic in the plane (this is the so-called 'equiaxed grain' hypothesis), the relevant components of the tensor P are identical to those given in eqns (4.5) of Ponte [START_REF] Ponte Castañeda | Variational estimates of the self-consistent type for some model nonlinear polycrystals[END_REF].

Some sample second-order self-consistent (SC) predictions for the effective flow stress, τ0 , are presented in figures 1 and 2 for various values of the nonlinearity exponent n, and the grain anisotropy parameter M = (τ 0 ) (2) /(τ 0 ) (1) . (An aggregate of 100 grain orientations was used to generate an isotropic texture in the transverse plane.) These predictions are compared against the Taylor and Sachs upper and lower bounds, the Hashin-Shtrikman (HS) upper bound of deBotton & Ponte Castañeda (1995) and the upper bound of [START_REF] Kohn | Some model problems of polycrystal plasticity with deficient basic crystals[END_REF]. (Explicit expressions for the Taylor, Sachs and Kohn-Little bounds, as well as numerical results for the HS bounds, have been given by Ponte [START_REF] Ponte Castañeda | Variational estimates of the self-consistent type for some model nonlinear polycrystals[END_REF] for this case.) The new SC estimates are also compared against the classical 'incremental' SC estimates of [START_REF] Hill | Continuum micro-mechanics of elastoplastic polycrystals[END_REF] and [START_REF] Hutchinson | Bounds and self-consistent estimates for creep of polycrystalline materials[END_REF], the 'secant' SC estimate of [START_REF] Berveiller | An extension of the self-consistent scheme to plastically-flowing polycrystals[END_REF], the 'tangent' (full anisotropic version) SC estimates of [START_REF] Molinari | A self-consistent approach of the large deformation polycrystal viscoplasticity[END_REF], the 'affine' SC estimate of [START_REF] Zaoui | Modeling stress-dependent transformation strains of heterogeneous materials[END_REF] and P. Suquet (1996, personal communication), as well as the 'variational' SC estimates of Ponte [START_REF] Ponte Castañeda | Variational estimates of the self-consistent type for some model nonlinear polycrystals[END_REF].

In figure 1a, b, results are shown for the various bounds and estimates for the effective flow stress τ0 as functions of the nonlinearity exponent, n, at fixed values of the grain anisotropy (M = 1 and 3, respectively). For M = 1, all the results-bounds and SC estimates-are in close agreement for n close to 1. The reason is that a twodimensional linear material with square symmetry is known to be isotropic, and the polycrystal then becomes a homogeneous isotropic material with shear modulus proportional to (τ 0 ) (1) . For M = 3, all the SC estimates agree in the limit as n approaches 1, but they become increasingly different as n increases. The following additional observations can be made.

= (τ 0 ) (2) /(τ 0 ) (1) = 1; (b) M = (τ 0 ) (2) /(τ 0 ) (1) = 3.
1. For low grain anisotropy (M = 1), the Taylor upper bound is sharper than the Kohn-Little bound. On the other hand, for the larger grain anisotropy (M = 3), the Kohn-Little bound improves on the Taylor bound for all values of n.

2. For M = 3, the 'incremental' SC estimate is seen to violate the Kohn-Little upper bound for values of n 10.

3. The rest of the SC estimates appear to satisfy the upper and lower bounds up to fairly large values of n. (Because of numerical error, in some cases it was not possible to generate results for n tending to ∞.) In general, the 'secondorder' SC estimates are the least stiff, with the 'tangent', 'affine' and 'variational' following in order of increasing stiffness. However, the 'tangent' SC estimates become extremely soft, tending to the Sachs lower bound, in the limit as n → ∞.

4. Two sets of results are shown here for the 'second-order' SC estimates: those obtained from the above-described dissipation potential formulation; and the corresponding estimates from the dual stress potential formulation (the latter are labelled U in figure 1 and appear as dashed lines). It is seen that, at least for these values of the grain anisotropy parameter, the two types of estimates are in very good agreement up to fairly large values of n. However, for sufficiently large n, the two sets of results begin to diverge with the stress potential estimates turning sharply toward the Taylor bound. Thus, in agreement with our earlier comments, the dissipation potential estimates appear to be more realistic.

In figure 2a, b, results are shown for the same bounds and estimates as in figure 1, but this time as functions of the grain anisotropy M , at fixed values of n (3 and 10). The following additional observations can be made. 1. The new 'second-order' SC estimates should be the most accurate at low grain anisotropy because of their exact asymptotic status for small contrast. In this sense, it would appear that all the other SC estimates tend to overestimate the effective flow stress of the nonlinear polycrystals at low grain anisotropy.

2. Although the 'affine' SC estimates were found to satisfy all bounds in the previous set of figures, it is seen here that, even at a fairly low value of n, the 'affine' SC estimates appear to violate the Kohn-Little bound at sufficiently high grain anisotropy. For the larger value of n, the 'affine' SC estimates break down at even lower values of the grain anisotropy. (Note, however, that the 'affine' method of [START_REF] Zaoui | Modeling stress-dependent transformation strains of heterogeneous materials[END_REF] can be implemented for elastic viscoplastic constitutive behaviour.) Similarly, the 'secant' SC estimates, which lie between the corresponding 'incremental' and 'affine' estimates, are seen to also violate the Kohn-Little bound. In conclusion, the 'variational', 'second-order' and 'tangent' SC estimates are the only that do not violate any bounds.

3. Because of their origin from a minimum principle (deBotton & Ponte Castañeda 1995), the 'variational' SC estimates should provide overestimates relative to the 'exact' SC estimates (i.e. those that would be obtained by means of the exact minimizing trial field in the context of the minimum principle). In this respect, the 'second-order' and 'tangent' SC estimates could be more accurate.

4. It is observed, however, that the 'tangent' SC estimates appear to satisfy a different scaling law than the 'second-order' and 'variational' SC estimates, which in turn appear to satisfy the same law as the Kohn-Little bound (i.e. square root in M ). Thus, it is seen that the 'tangent' SC estimates reach a limiting state beyond which further increases in M lead to no corresponding increases in the effective flow stress. While strictly unable to rule it out, this behaviour, especially for the low value of n (n = 3), would appear to be unrealistically soft.

Concluding remarks

In conclusion, the 'second-order' SC estimates-those obtained from the dissipation potential version (3.11) of the theory-would appear to be the most accurate of all, certainly when compared to the 'classical' SC estimates, and probably also when compared to other recently proposed SC estimates. This statement would be rigorously true at low grain anisotropy, but would still need to be proved more generally.

In this connection, lower bounds that are sharper than Sachs, such as those that have been proposed by [START_REF] Talbot | Bounds of third order for the overall response of nonlinear composites[END_REF] for two-phase nonlinear composites, would be extremely useful. Similarly, comparisons with direct numerical simulations could also be very insightful.

This work was supported by NSF grant no. CMS-96-22714. We are grateful to Renaud Masson for valuable discussions concerning the numerical implementation of the various schemes.

Figure 1 .

 1 Figure 1. Comparison of the new second-order self-consistent estimates with various bounds and other self-consistent estimates for the effective flow stress τ0 , as functions of n. Values of the grain anisotropy: (a) M = (τ 0 ) (2) /(τ 0 ) (1) = 1; (b) M = (τ 0 ) (2) /(τ 0 ) (1) = 3.

Figure 2 .

 2 Figure 2. Comparison of the new second-order self-consistent estimates with various bounds and other self-consistent estimates for the effective flow stress, τ0 , as functions of the grain anisotropy, M = (τ 0 ) (2) /(τ 0 ) (1) . (a) n = 3; (b) n = 10.


David Nowak

Yu Zhang

Formal Security Proofs with Minimal Fuss: Implicit Computational Complexity at Work $

Keywords: lambda-calculus, safe recursion, probabilistic computation, cryptography 2010 MSC: 03B40, 03D15, 60E05, 94A60

We show how implicit computational complexity can be used in order to increase confidence in game-based security proofs in cryptography. For this purpose we extend CSLR, a probabilistic lambda-calculus with a type system that guarantees the existence of a probabilistic polynomial-time bound on computations. This allows us to define cryptographic constructions, feasible adversaries, security notions, computational assumptions, game transformations, and gamebased security proofs in a unified framework. We also show that the standard practice of cryptographers, ignoring that polynomial-time Turing machines cannot generate all uniform distributions, is actually sound. We illustrate our calculus on cryptographic constructions for public-key encryption and pseudorandom bit generation.

Introduction

When a new cryptographic scheme is published, it often comes with a security proof. It is unfortunately common that such schemes are vulnerable even though they have been supposedly proved secure -attacks are often found a few months or a few years after publication of the so-called security proof. This presents a serious demand for formal, ideally automated verification of security proofs in cryptography, which is well-known and acknowledged by cryptographers [START_REF] Halevi | A plausible approach to computer-aided cryptographic proofs[END_REF].

It is good practice to structure security proofs as a sequence of game transformations since it makes easier their checking by a third party [START_REF] Bellare | Code-based game-playing proofs and the security of triple encryption[END_REF][START_REF] Shoup | Sequences of games: a tool for taming complexity in security proofs[END_REF]. In this game-based approach, a security property is modeled as a probabilistic program implementing a game to be solved by the adversary. The adversary itself is modeled as an external probabilistic procedure interfaced with the game. Proving security amounts to proving that any adversary has at most a negligible advantage over an adversary playing against a perfectly secure scheme.

If however the adversary were given unlimited computational power, then it could break most cryptographic schemes without making them insecure in practice. It is thus necessary to restrict the computational power of the adversary so that the attacks are feasible. Cobham's thesis asserts that being feasible is the same as being computable in polynomial time [START_REF] Cobham | The intrinsic computational difficulty of functions[END_REF]. Cryptographers follow Cobham's thesis in their security proofs by assuming that the adversary is computable in probabilistic polynomial time (for short, PPT), i.e., executable on a Turing machine extended with a read-only random tape that has been filled with random bits, and working in (worst-case) polynomial time. One way to take complexity into account in formal verification would be to formalize a precise execution model (e.g., Turing machines) and to explicitly count the number of steps necessary for the execution of the algorithm. Such approach would for the least be tedious and would give results depending on the particular execution model in use whereas one is mainly interested in the complexity class independent of execution models. Implicit computational complexity suggests a more convenient approach, which relates computations and/or programming languages with complexity classes without relying on specific execution models nor explicit counting of execution steps.

Although the languages of CertiCrypt [START_REF] Barthe | Formal certification of code-based cryptographic proofs[END_REF], EasyCrypt [START_REF] Barthe | Computer-Aided Security Proofs for the Working Cryptographer[END_REF] or CryptoVerif [START_REF] Blanchet | Automated security proofs with sequences of games[END_REF] can be used for writing game-based security proofs, a language that can automatically take into account complexity issues is still missing. In this paper we show how Computational SLR [START_REF] Zhang | The Computational SLR: a logic for reasoning about computational indistinguishability[END_REF] (for short, CSLR), a probabilistic lambdacalculus with a type system that guarantees that computations are PPT, can be extended so as to allow for defining cryptographic constructions, feasible adversaries, security notions, computational assumptions, game transformations, and game-based security proofs in a unified framework.

In implementations of cryptographic schemes, because computers are based on binary digits, the cardinal of the support of a uniform distribution has to be a power of 2. Even at a theoretical level, probabilistic Turing machines used in the definition of PPT choose random numbers only among sets of cardinal a power of 2 [START_REF] Goldreich | The Foundations of Cryptography: Basic Tools[END_REF]. In the case of another cardinal, the uniform distribution can only either be approximated or rely on code that is not guaranteed to terminate, although it will terminate with a probability arbitrarily close to 1 [START_REF] Hurd | A formal approach to probabilistic termination[END_REF]. With arbitrary random choices that are used in games, one can define more distributions than those allowed by the definition of PPT. This raises a fundamental concern that is usually overlooked by cryptographers.

Related work. Over the last years, apart from the ones already mentioned above, other frameworks for machine-checking security proofs in cryptography have been proposed [START_REF] Backes | A formal language for cryptographic pseudocode[END_REF][START_REF] Barthe | Computational Indistinguishability Logic[END_REF][START_REF] Corin | A probabilistic Hoare-style logic for gamebased cryptographic proofs[END_REF][START_REF] Courant | Towards automated proofs for asymmetric encryption schemes in the random oracle model[END_REF][START_REF] Nowak | A framework for game-based security proofs[END_REF][START_REF] Nowak | On formal verification of arithmetic-based cryptographic primitives[END_REF]. However, these frameworks either ignore complexity-theoretic issues or postulate the complexity of the involved functions. More recently, in [START_REF] Heraud | A formalization of polytime functions[END_REF], Heraud and Nowak present their formalization in the proof assistant Coq of Bellantoni and Cook's characterization of the class of polytime functions [START_REF] Bellantoni | A new recursion-theoretic characterization of the polytime functions[END_REF]. They show how their formalization can be used to deal with the complexity bound on the adversary in Nowak's toolbox [START_REF] Nowak | A framework for game-based security proofs[END_REF][START_REF] Nowak | On formal verification of arithmetic-based cryptographic primitives[END_REF], and extend CertiCrypt [START_REF] Barthe | Formal certification of code-based cryptographic proofs[END_REF] so as to alleviate the need for postulating the complexity of functions.

Since Bellantoni and Cook's characterization, there have been other ones. For instance, a recent one is given in [START_REF] Marion | A type system for complexity flow analysis[END_REF].

Mitchell et al. have proposed a process calculus with bounded replications and messages to guarantee that processes are computable in polynomial time [START_REF] Mitchell | A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols[END_REF]. Messages can be terms of OSLR -Hofmann's SLR [START_REF] Hofmann | A Mixed Modal/Linear Lambda Calculus with Applications to Bellantoni-Cook Safe Recursion[END_REF] with a random oracle [START_REF] Mitchell | A linguistic characterization of bounded oracle computation and probabilistic polynomial time[END_REF]. Their calculus aim at being general enough to deal with cryptographic protocols, whereas we aim at a simpler calculus able to deal with cryptographic constructions.

Impagliazzo and Kapron have proposed two logics for reasoning about cryptographic constructions [START_REF] Impagliazzo | Logics for reasoning about cryptographic constructions[END_REF]. The first one is based on a non-standard arithmetic model, which, they prove, captures probabilistic polynomial-time computations. The second one is built on top of the first one, with rules justifying computational indistinguishability.

The above approaches are limited to the verification of cryptographic algorithms, and cannot deal with their implementations. This issue has been tackled by Affeldt et al. in [START_REF] Affeldt | Certifying assembly with formal cryptographic proofs: the case of BBS[END_REF] where it is shown how game-based security proofs can be conducted directly on implementations in assembly language.

Another probabilistic variant of Hofmann's SLR is proposed in [START_REF] Lago | A Higher Order Characterization of Probabilistic Polynomial Time[END_REF]. In contrast to OSLR [START_REF] Mitchell | A linguistic characterization of bounded oracle computation and probabilistic polynomial time[END_REF] and CSLR [START_REF] Zhang | The Computational SLR: a logic for reasoning about computational indistinguishability[END_REF], the bound on the reduction time is here proved by syntactical means and thus makes explicit a notion of evaluation in polynomial time. However, for our purpose, it is enough to know that an adversary could be executed in polynomial time: we do not need an explicit reduction. Therefore, as it is the case with SLR and OSLR, there is no operational semantics for CSLR.

Contributions. We demonstrate the usefulness of implicit computational complexity in cryptography by writing game-based security proofs with CSLR, a lambda calculus whose type system allows for restricting the computational power of the adversary so that its attacks are feasible. By completeness, any adversary can be defined as a CSLR term of a certain type. Our approach has the advantage that it can automatically prove (by type inference [START_REF] Hofmann | A Mixed Modal/Linear Lambda Calculus with Applications to Bellantoni-Cook Safe Recursion[END_REF]) that a program is PPT.

We show that the standard practice of cryptographers, ignoring that polynomial-time Turing machines cannot generate all uniform distributions, is actually sound.

With respect to feasible adversaries, we define a notion of game indistinguishability. Although, it is not stronger than the notion of computational indistinguishability of [START_REF] Zhang | The Computational SLR: a logic for reasoning about computational indistinguishability[END_REF], it is simpler to prove and well-suited for formalizing game-based security proofs. We indeed show that this notion allows to easily model security definitions and computational assumptions. Moreover we show that computational indistinguishability implies game indistinguishability, so that we can reuse as it is the equational proof system of [START_REF] Zhang | The Computational SLR: a logic for reasoning about computational indistinguishability[END_REF]. More precisely, the former allows for any arbitrary use of the compared program by the adversary, while the latter provides more control over the adversary as it is usual in game-based security definitions, thus making game indistinguishability adequate.

CSLR, as initially defined by Zhang [START_REF] Zhang | The Computational SLR: a logic for reasoning about computational indistinguishability[END_REF], does not allow superpolynomialtime computations (i.e., computations that are not bounded above by any polynomial) nor arbitrary uniform choices. Although this restriction makes sense for the cryptographic constructions and the adversary, the game-based approach to cryptographic proofs does not preclude the possibility of introducing games that perform superpolynomial-time computations or that use arbitrary uniform distributions. They are just idealized constructions that are used to define security notions but are not meant to make their way into implementations. We thus extend CSLR into CSLR $ π that includes CSLR as a sublanguage and that allows for superpolynomial-time computations and arbitrary uniform choices.

We illustrate the usability of our approach by proving formally in our proof system that the public-key encryption scheme ElGamal [START_REF]A public key cryptosystem and a signature scheme based on discrete logarithms[END_REF] and the pseudorandom bit generator of Blum, Blum and Shub [START_REF] Blum | A simple unpredictable pseudo-random number generator[END_REF] (for short, BBS) are secure in the appropriate senses stated by cryptographers [START_REF] Goldwasser | Probabilistic encryption[END_REF][START_REF] Blum | A simple unpredictable pseudo-random number generator[END_REF] and formalized here.

Outline. We introduce CSLR in Section 2. In Section 3, we discuss the problem of approximating uniform sampling from sets of arbitrary size using just fair coin tosses, and study the relation with perfect uniform sampling. In Section 4, we add the possibility of introducing superpolynomial-time primitives for defining security notions and equip the calculus with a notion of game indistinguishability. In Section 5, we illustrate the use of our calculus by proving formally with it the semantic security the ElGamal encryption scheme and the unpredictability of the Blum-Blum-Shub pseudorandom bit generator. Finally, we conclude in Section 6.

Computational SLR

Bellantoni and Cook have proposed to replace the model of Turing machines by their safe recursion scheme which defines exactly functions that are computable in polynomial time on a Turing-machine [START_REF] Bellantoni | A new recursion-theoretic characterization of the polytime functions[END_REF]. This is an intrinsic, purely syntactic mechanism: variables are divided into safe variables and normal variables, and safe variables must be instantiated by values that are computed using only safe variables; recursion must take place on normal variables and intermediate recursion results are never sent to normal variables. When higher-order recursors are concerned, it is also required that step functions must be linear, i.e., intermediate recursive results can be used only once in each step. Thanks to those syntactic restrictions, exponential-time computations are avoided. This is an elegant approach in the sense that polynomial-time computation is characterized without explicitly counting the number of computation steps.

Hofmann later developed a functional language called SLR to implement safe recursion [START_REF] Hofmann | A Mixed Modal/Linear Lambda Calculus with Applications to Bellantoni-Cook Safe Recursion[END_REF][START_REF] Hofmann | Safe recursion with higher types and BCK-algebra[END_REF]. It provides a complete characterization through typing of the complexity class of probabilistic polynomial-time computations. He introduces a type system with modality to distinguish between normal variables and safe variables, and linearity to distinguish between normal functions and linear functions. He proves that well-typed functions of a proper type are exactly polynomial-time computable functions. Moreover there is a type-inference algorithm that can automatically determine the type of any expression [START_REF] Hofmann | A Mixed Modal/Linear Lambda Calculus with Applications to Bellantoni-Cook Safe Recursion[END_REF]. Mitchell et al. have extended SLR by adding a random bit oracle to simulate the oracle tape in probabilistic Turing-machines [START_REF] Mitchell | A linguistic characterization of bounded oracle computation and probabilistic polynomial time[END_REF].

More recently, Zhang has introduced CSLR, a non-polymorphic version of SLR extended with probabilistic computations and a primitive notion of bitstrings [START_REF] Zhang | The Computational SLR: a logic for reasoning about computational indistinguishability[END_REF]. His use of monadic types [START_REF] Moggi | Notions of computation and monads[END_REF], allows for an explicit distinction in CSLR between probabilistic and purely deterministic functions. This distinction was not possible with the extension by Mitchell et al. [START_REF] Mitchell | A linguistic characterization of bounded oracle computation and probabilistic polynomial time[END_REF].

The language CSLR

We recall below the definition of CSLR and its main properties.

Types. Types are defined by: τ, τ , . . .

::= Bits | τ × τ | τ → τ | τ → τ | τ τ | Tτ
Bits is the base type for bitstrings. The monadic types Tτ capture probabilistic computations that produce a result of type τ . All other types are from Hofmann's SLR [START_REF] Hofmann | Safe recursion with higher types and BCK-algebra[END_REF]. τ × τ are cartesian product types. There are three kinds of functions: τ → τ are types for modal functions with no restriction on the use of their argument; τ → τ are types for non-modal functions where the argument must be a safe value; τ τ are types for linear functions where the argument can only be used once. Note that linear types are not necessary when we do not have higher-order recursors, which are themselves not necessary for characterizing PTIME computations but can ease and simplify the programming of certain functions (such as defining the Blum-Blum-Shub pseudorandom bit generator in Section 4.4).

CSLR also has a sub-typing relation <: between types. In particular, the sub-typing relation between the three kinds of functions is: τ τ <: τ → τ <: τ → τ . We also have Bits → τ <: Bits τ , stating that bitstrings can be duplicated without violating linearity. The subtyping relation is inherited from SLR, with an additional rule saying that the constructor T preserves subtyping [START_REF] Zhang | The Computational SLR: a logic for reasoning about computational indistinguishability[END_REF].

Expressions. Expressions of CSLR are defined by the following grammar: e 1 , e 2 , . . . otherwise, where n is the part of the bitstring n with its first bit cut off. rand returns a random bit 0 or 1, each with the probability 1 2 . return(e) is the trivial computation which returns e with probability 1. We note that CSLR has no restriction on e in general -it can be a probabilistic computation too (of type Tτ ), in which case return(e) will be of type TTτ . bind x ← e 1 in e 2 is the sequential computation which first computes the probabilistic computation e 1 , binds its result to the variable x, then computes e 2 . All other expressions are from Hoffman's SLR [START_REF] Hofmann | Safe recursion with higher types and BCK-algebra[END_REF].

::= x | nil | B 0 | B 1 | case τ | rec τ | λx.e |
To ease the reading of CSLR terms, we shall use some syntactic sugar and abbreviations in the rest of the paper:

• λ . e represents λx . e when x does not occur as a free variable in e; where e 1 is a distribution in which a value x is chosen at random; = and tail tail tail are respectively the equality test between two bitstrings and the function that remove the left-most bit from a bitstring. These functions can be defined in CSLR [START_REF] Zhang | The Computational SLR: a logic for reasoning about computational indistinguishability[END_REF].

• x ←
Type system. Typing assertions of expressions are of the form Γ t : τ , where Γ is a typing context that assigns types and aspects (inherited from Hofmann's system) to variables. Intuitively, an aspect specifies how the variable can be used in the program. For instance, a linear aspect forces that the variable can be used only once. A typing context is typically written as a list of bindings x 1 : a1 τ 1 , . . . , x n : an τ n , where a 1 , . . . a n are aspects. The type system for CSLR can be found in [START_REF] Zhang | The Computational SLR: a logic for reasoning about computational indistinguishability[END_REF].

Operational semantics. We can define a reduction system for the computational SLR, and prove that every closed term has a canonical form. In particular, the canonical form of type Bits is:

b ::= nil | B 0 b | B 1 b.
If u is a closed term of type Bits, we write |u| for its length. We define the length of a bitstring on its canonical form b:

|nil| = 0, |B i b| = |b| + 1 (i = 0, 1).
If e is a closed program of type TBits and all possible results of e are of the same length, we write |e| for the length of its result bitstrings.

The language deals with bitstrings, but in many discussions of cryptography, it will be more convenient to see them as integers. We write b for the integer value of the bitstring b.

Denotational semantics. The denotational semantics of CSLR is defined based on a set-theoretic model [START_REF] Zhang | The Computational SLR: a logic for reasoning about computational indistinguishability[END_REF]. We write B for the set of bitstrings. To interpret the probabilistic computations, we adopt the probabilistic monad defined in [START_REF] Ramsey | Stochastic lambda calculus and monads of probability distributions[END_REF]: if A is a set, we write D A : A → [0, 1] for the set of probability mass functions over A. The original monad in [START_REF] Ramsey | Stochastic lambda calculus and monads of probability distributions[END_REF] is defined using measures instead of mass functions, and is of type

(2 A → [0, ∞]) → [0, ∞],
where 2 A denotes the set of all subsets of A, so that it can also represent computing probabilities over infinite data structures, not just discrete probabilities. But for the sake of simplicity, in this paper as well as in [START_REF] Zhang | The Computational SLR: a logic for reasoning about computational indistinguishability[END_REF] we work on mass functions instead of measures. Note that the monad is not the one defined in [START_REF] Mitchell | A linguistic characterization of bounded oracle computation and probabilistic polynomial time[END_REF], which is used to keep track of the bits read from the oracle tape rather than reasoning about probabilities.

When d is a mass function of D A and a ∈ A, we also write Pr[d a] for the probability d(a). If there are finitely many elements in d ∈ D A , we can write d as {(a 1 , p 1 ), . . . , (a n , p n )}, where a i ∈ A and p i = d(a i ). When we restrict ourselves to finite distributions, our monad becomes identical to the one used in [START_REF] Nowak | A framework for game-based security proofs[END_REF][START_REF] Nowak | On formal verification of arithmetic-based cryptographic primitives[END_REF].

With this monad, every computation type Tτ in CSLR will be interpreted as D τ , where τ is the interpretation of τ . Expressions are interpreted within an environment which maps every free variable to an element of the corresponding type. In particular, the two computational constructions are interpreted as:

return(e) ρ = {( e ρ , 1)} x $ ← e 1 ; e 2 ρ = λv . v ∈ τ e 2 ρ[x →v ] (v) × e 1 ρ (v )
where τ is the type of x (or Tτ is the type of e 1 ). Interpretation of other types and expressions is given in [START_REF] Zhang | The Computational SLR: a logic for reasoning about computational indistinguishability[END_REF].

The main property of CSLR [START_REF] Mitchell | A linguistic characterization of bounded oracle computation and probabilistic polynomial time[END_REF][START_REF] Zhang | The Computational SLR: a logic for reasoning about computational indistinguishability[END_REF] is:

Theorem 1.
The set-theoretic interpretations of closed terms of type Bits → TBits in CSLR are exactly the functions that can be computed by a probabilistic Turing machine in polynomial time.

This theorem implies that CSLR is expressive enough to model an adversary and to implement cryptographic constructions, as they both are probabilistic polynomial-time functions. We remark that adversaries can return values of types other than Bits (e.g., tuples of bitstrings), but we can always define adversaries as a PPT function of type Bits → TBits by adopting some encoding of different types of values into bitstrings, so the theorem still applies. The same is true in case of functions with multiple arguments: we can uncurrify them and then adopt some encoding so that the theorem still applies.

The development of our system is based on CSLR. We often need to state that some functions are deterministic, however it is not sufficient to say the such functions are of non-monadic type (types with no constructor T), e.g., Bits → Bits. Because the language is functional, it is easy to define functions of non-monadic functions that involve probabilistic computations, for instance, λx . ((λy . 1)rand). To specify a deterministic function in our system, we explicitly state that it is definable (and/or typable) in SLR.

An example of PPT function. The random bitstring generation is defined as follows:

rs rs rs def = λn . if (n ? = nil) then return(nil) else b $ ← rand; u $ ← rs rs rs(tail tail tail (n)); return(b•u)
where • denotes the concatenation operation of bitstrings, which can be programmed and typed in CSLR [START_REF] Zhang | The Computational SLR: a logic for reasoning about computational indistinguishability[END_REF]. rs rs rs receives a bitstring and returns a uniformly random bitstring of the same length. It can be checked that rs rs rs : Bits → TBits.

Computational indistinguishability.

A notion of computational indistinguishability in cryptography has been defined in the CSLR system [START_REF] Zhang | The Computational SLR: a logic for reasoning about computational indistinguishability[END_REF].

Definition 1 (Computational indistinguishability). Two CSLR terms f 1 and f 2 , both of type Bits → τ , are computationally indistinguishable (written as f 1 f 2 ) if for every closed CSLR term A of type Bits → τ → TBits and every positive polynomial P , there exists some N ∈ N such that for all bitstrings

η with |η| ≥ N |Pr[ A(η, f 1 (η)) 1] -Pr[ A(η, f 2 (η)) 1]| < 1 P (|η|)
This definition is a reformulation of Definition 3.2.2 of [START_REF] Goldreich | The Foundations of Cryptography: Basic Tools[END_REF] in CSLR. In particular, a CSLR term of type Bits → Tτ defines a so-called probabilistic ensemble. An equational proof system that can demonstrate computational indistinguishability between CSLR programs is also defined in [START_REF] Zhang | The Computational SLR: a logic for reasoning about computational indistinguishability[END_REF]. The proof system consists of rules justifying semantic equivalence, and rules justifying computational indistinguishability. Program equivalence is written as e 1 ≡ e 2 , indicating that e 1 and e 2 have the same denotation. In Figure 1, we list the proof rules that will be used in this paper. Please refer to [START_REF] Zhang | The Computational SLR: a logic for reasoning about computational indistinguishability[END_REF] for the full proof system.

Rules justifying semantic equivalence:

AX-BIND-1 x $ ← return(e1); e2 ≡ e2[e1/x] AX-BIND-2 x $ ← e; return(x) ≡ e AX-BIND-3 x $ ← (y $ ← e1; e2); e3 ≡ y $ ← e1; x $ ← e2; e3 e ≡ e VAL return(e) ≡ return(e ) e1 ≡ e 1 e2 ≡ e 2 BIND x $ ← e1; e2 ≡ x $ ← e 1 ; e 2
Rules justifying computational indistinguishability:

ei : Bits → τ (i = 1, 2) e1 ≡ e2 EQUIV e1 e2 ei : Bits → τ (i = 1, 2,

Uniform sampling

As it is the case for computers, CSLR has binary digits as its fundamental representation of data. While uniform distributions are ubiquitous in cryptography, binary representation does not support an exact implementation of an arbitrary uniform distribution, particularly when the cardinal of its support is not a power of 2. This section discusses the approximation of uniform sampling in the setting of CSLR, and introduces an extension CSLR $ that includes a uniform sampling primitive.

Modeling uniform sampling in CSLR

In modern computers based on binary digits, implementing uniform distributions requires that the cardinal of the support of a uniform distribution should be a power of 2. In case of a different cardinal, such a distribution can be approximated by repeatedly selecting a random value in a larger distribution whose cardinal is a power of 2, until one obtain a value in the desired range or reach the maximal number of allowed attempts (timeout, which determines the precision of the approximation). In the latter case a default value is returned. 1We implement this pseudo-uniform sampling in CSLR as follows:

zrand zrand zrand def = λn . λt . if t ? = nil then return(0 |n| ) else v $ ← rs rs rs(n); if v ≥ n then zrand zrand zrand (n, tail tail tail (t)) else return(v)
The program takes two arguments: the sampling range (represented by the value n) and the timeout (represented by |t|). The test ≥ can be programmed in CSLR. The timeout is represented by the length of the bitstring t for the sake of simplicity and readability of the program, but an alternative representation of using t as the timeout is certainly acceptable. The program zrand zrand zrand uses u = 2 log 2 n as the cardinal of the larger distribution and makes samplings in this distribution. The probability that one sampling falls outside the desired range is u-n u , thus probability that |t| consecutive attempts fail is u-n u |t| . zrand zrand zrand will return 0 |n| as the default value after |t| consecutive failures, so the probability that a value smaller than n but other than 0 |n| is returned is

1-( u-n u ) |t| n
, and the probability that 0 |n| is returned is

1+( n-1)•( u-n u ) |t| n .
Similarly, a finite group can be encoded in CSLR and multiplication and group exponentiation can be programmed (as implied by Theorem 1). In the sequel, we shall write Z q (q a bitstring) for the set of bitstrings (of the same length than q) of {0, 1, . . . , q -1}, and Z $ q for the truly uniform distribution from Z q .

CSLR $

CSLR $ extends CSLR with a uniform sampling primitive sample of type Bits TBits. sample receives a bitstring as argument and returns uniformly a random bitstring of the same length whose integer value is strictly smaller than that of the argument, i.e., sample(q) = Z $ q for every bitstring q. For instance, the distribution produced by sample(101) is

sample(101) = {(000, 1 5
), . . . , (100,

We can program a sampling from an arbitrary finite set (of CSLR definable elements, usually just bitstrings in cryptography) using sample, assuming that there is an index function over the set.

The type system of CSLR $ is extended with only the proper rules for sample and constants. Note that the type of sample is Bits TBits so that it can accept arguments that are defined using linear resources.

The following lemma justifies the use of zrand zrand zrand to approximate the uniform sampling from Z q : Lemma 1. Let q be a closed CSLR term of type Bits → Bits. The probabilistic ensembles λη . zrand zrand zrand (q(η), η) and λη . sample(q(η)) are computationally indistinguishable, i.e., for every closed CSLR term A of type Bits → τ → TBits and every positive polynomial P , there exists some N ∈ N such that for all bitstrings η with |η| ≥ N |Pr[ A(η, zrand zrand zrand (q(η), η))

1] -Pr[ A(η, sample(q(η))) 1]| < 1 P (|η|)
.

Proof. We show that the two ensembles are statistically close:

1 2 • Σ v∈Z q(η) |Pr[ zrand zrand zrand (q(η), η) v] -Pr[ sample(q(η)) v]| = 1 2 • Σ v∈Z q(η) Pr[ zrand zrand zrand (q(η), η) v] -Pr[Z $ q(η) v] = 1 2 • 1 + ( q(η) -1) • ε q(η) - 1
q(η) + ( q(η) -1) • 1 -ε q(η) - 1 q(η) = q(η) -1 q(η)
• ε is negligible with respect to |η|, where ε = 2 log 2 q(η) -q(η)

2 log 2 q(η) |η| ≤ (1/2) |η| .
We can then conclude because statistical closeness implies computational indistinguishability (cf. Section 3.2.2 of [START_REF] Goldreich | The Foundations of Cryptography: Basic Tools[END_REF]).

In Lemma 1, the security parameter η is used directly as the timeout of zrand zrand zrand . A more general implementation would instantiate the timeout by a polynomial of |η|, i.e., zrand zrand zrand (q(η), p(η)) where p is a well-typed SLR function of type Bits → Bits. The choice of p will affect the final distribution of the program and consequently the advantage of adversaries in security experiments, but that remains negligible. It is possible to use CSLR to deal with exact security and the exact timeout with p is necessary in that case.

We say a CSLR program P with a free variable s of type Bits → TBits is a s-sampling-based program if every occurence of the free variable s is in an application s(t), with t an arbitrary CSLR term of type Bits. We call s the sampling function variable. The purpose of this definition is to be able to exclude higher-order arguments such as zrand zrand zrand or sample in the next proposition.

If a CSLR $ program P can be obtained from a s-sampling-based CSLR program P by replacing all s with sample, i.e., P = P [sample/s], we say that P is a well-formed sampling program.

Consider the computational indistinguishability as defined in Definition 1, but now programs (except for adversaries) can be defined in CSLR $ , i.e., their definitions can include the primitive sample. Lemma 1 implies that we can freely replace the approximate uniform sampling zrand zrand zrand by the truly uniform sampling sample or vice versa in sampling-based CSLR programs, without affecting the computational indistinguishability. Proof. First, it is easy to show that for n pairs of computationally indistinguishable CSLR programs (f

• Q by replacing each subterm v i in Q by a projection proj i (v) with v a fresh variable, i.e., Q = Q [proj 1 (v)/v 1 , . . . , proj n (v)/v n ].
Clearly, Q is still a CSLR program and

P (η)[sample/s] ≡ Q(η)[(sample(t 1 ), . . . , sample(t n ))/v] P (η)[λx . zrand zrand zrand (x, η)/s] ≡ Q(η)[(zrand zrand zrand (t 1 , η), . . . , zrand zrand zrand (t n , η))/v]
where ≡ denotes program equivalence as defined in the proof system of CSLR in [START_REF] Zhang | The Computational SLR: a logic for reasoning about computational indistinguishability[END_REF]. For an arbitrary CSLR adversary

))) 1]|
is negligible since A is also a valid CSLR adversary.

Uniform computational indistinguishability

The definition of computational indistinguishability (as in Definition 1 or its original form in cryptography, e.g., Definition 3.2.2 in [START_REF] Goldreich | The Foundations of Cryptography: Basic Tools[END_REF]) enforces that adversaries must be in the complexity class PPT. In our setting, it means that an adversary must be definable in the original CSLR without using the primitive sample. However it is a standard practice of cryptographers to ignore that polynomial-time Turing machines cannot generate all distributions. We formally show in this section that this practice is actually sound. Indeed, we can allow adversaries to use uniform sampling primitive sample and such adversaries gain no significantly larger capability than PPT adversaries in terms of computational indistinguishability.

Let A be a closed CSLR $ program of type Bits → τ → TBits with τ an arbitrary type. We call A a uniform adversary if every occurence of sample is in an application sample(t) for some subterm t.

Definition 2 (Uniform comp. ind.). Two CSLR $ terms f 1 and f 2 , both of type Bits → τ , are uniform computationally indistinguishable (written as f 1 $ f 2 ) if for every uniform adversary A of type Bits → τ → TBits and every positive polynomial P , there exists some N ∈ N such that for all bitstrings η with |η| ≥ N

|Pr[ A(η, f 1 (η)) 1] -Pr[ A(η, f 2 (η)) 1]| < 1 P (|η|)
.

For the sake of clarity, we shall sometimes refer to the original definition of computational indistinguishability where adversaries are not allowed to use sample as PPT-computational indistinguishability. The following proposition states that uniform computational indistinguishability is equivalent to PPTcomputational indistinguishability.

Proposition 2. For every pair of well-formed sampling CSLR $ programs P 1 , P 2 of type Bits → τ , P 1 P 2 if and only if P 1 $ P 2 .

Proof. Clearly every PPT adversary is also a uniform adversary whose definition does not include sample, hence uniform computational indistinguishability implies PPT-computational indistinguishability.

In the proof, we write

Pr[ Q 1 1] . = Pr[ Q 2 1] if |Pr[ Q 1 1] -Pr[ Q 2 1]
| is negligible w.r.t. parameter |η|, where η appears as a bitstring in Q 1 and Q 2 .

For the reverse direction, with an arbitrary uniform adversary A, we define

A = λη . A[λx . zrand zrand zrand (x, η)/sample], P i = λη . P i (η)[λx . zrand zrand zrand (x, η)/sample].
Clearly, A is a PPT adversary and we have

A (η, P i (η)) ≡ A(η, P i (η))[λx . zrand zrand zrand (x, η)/sample].
We can prove that

Pr[ A(η, P 1 (η)) 1] . = Pr[ A (η, P 1 (η))
1] (by Proposition 1, A(η, P 1 (η)) A (η, P 1 (η))) . = Pr[ A (η, P 1 (η) ) 1] (by Proposition 1, P 1 P 1 and A being the PPT adversary) . = Pr[ A (η, P 2 (η) ) 1] (by hypothesis P 1 P 2 and A being the PPT adversary) . = Pr[ A (η, P 2 (η) ) 1] (by Proposition 1, P 2 P 2 and A being the PPT adversary) . = Pr[ A(η, P 2 (η) ) 1] (by Proposition 1, A(η, P 2 (η)) A (η, P 2 (η))), therefore P 1 $ P 2 .

Proposition 2 suggests that we can replace the notion of computational indistinguishability with the more general notion of uniform computational indistinguishability and use the CSLR proof system as it is.

A game-based proof system

CSLR by itself only considers computations based on binary digits and does not allow superpolynomial-time computations. Section 3 shows that we can introduce uniform sampling into CSLR and the proof system for computational indistinguishability remains valid. The complexity restriction makes sense for the cryptographic constructions and the adversary, however the game-based approach to cryptographic proofs does not preclude the possibility of introducing games that perform superpolynomial-time computations -they are just idealized constructions that are used to define security notions but are not meant to make their way into implementations.

In this section, we extend CSLR both with superpolynomial-time computations and arbitrary uniform choices.

CSLR

$ π CSLR $
π extends CSLR with the uniform sampling primitive sample and a set π of superpolynomial-time primitives.

The type system of CSLR $ π is extended with only the proper rules for sample and superpolynomial-time constants in π. Note that in CSLR $ π we do not care any more about the complexity class that can be characterized using the type system 2 -the language and type system of CSLR $ π are there for defining and describing security notions, not adversaries.

2 Nevertheless, one might expect that the complexity class characterized by CSLR $ π is P P T X , where X is the smallest complexity class in which additional constants can be defined, but the exact relation between CSLR $ π and the complexity classes remains to be clarifiedthe addition of the primitive sample alone allows for defining more distributions than in PPT.

We adopt the notion of uniform computational indistinguishability in Section 3.3, except that in CSLR $ π we are considering indistinguishability between CSLR $ π programs. Adversaries remains uniform adversaries that are definable in CSLR $ . Definition 3 (Comp. ind. in CSLR $ π ). Two CSLR $ π terms f 1 and f 2 , both of type Bits → τ , are computationally indistinguishable (written as f 1 $ π f 2 ) if for every uniform adversary A of type Bits → τ → TBits that is definable in CSLR $ , and every positive polynomial P , there exists some N ∈ N such that for all bitstrings η with |η| ≥ N

|Pr[ A(η, f 1 (η)) 1] -Pr[ A(η, f 2 (η)) 1]| < 1 P (|η|)
.

We call a probability distribution D over bitstrings a CSLR $ π distribution, if it can be realized by a CSLR $ π program (normally with sample), i.e., a closed CSLR $ π term e of type TBits such that e = D, and we write D for the CSLR $ π program that realizes the distribution.

For every closed CSLR $ π program e of type Tτ , we write samp (e) for the sample space of e , i.e., the set of all values of τ which e returns with nonzero probability.

Lemma 2. For every pair of uniform CSLR

$ π distributions C and D, if f is a CSLR $ π function of type Bits → Bits such that f is a n-to-1 surjection from samp (C) to samp (D), then x $ ← C ; return(f (x)) ≡ D .
Proof. The distribution of the lefthand side is

x $ ← C ; return(f (x)) = {( f (v), n × 1 | samp (C)| ) | v ∈ samp (C)}.
Because f is a n-to-1 surjection from samp (C) to samp (D), we have

| samp (C)| = n • | samp (D)|,
and it is clear that the above distribution equals D.

Game indistinguishability

The notion of computational indistinguishability already allows us to perform some cryptographic proofs as shown in [START_REF] Zhang | The Computational SLR: a logic for reasoning about computational indistinguishability[END_REF], but many cryptographers advocate the so-called game-based approach which structures security proofs as a sequence of game transformations [START_REF] Bellare | Code-based game-playing proofs and the security of triple encryption[END_REF][START_REF] Shoup | Sequences of games: a tool for taming complexity in security proofs[END_REF] and computational indistinguishability is not a practical notion for game-based proofs. CSLR $ π can help to formalize game transformations and makes it feasible to automate the proof checking procedure.

In game-based proofs, an adversary involved in a game can be an arbitrary probabilistic polynomial-time program, hence it can be encoded as a well-formed CSLR $ sampling program of type Bits → Tτ , where the security parameter will bound its running time, and τ is the type of messages returned by the adversary. A game is encoded as a closed, well-formed CSLR $ π sampling function of type Bits → ( Bits → Tτ ) → TBits that takes the security parameter and the adversary as arguments and returns one bit denoting whether the adversary wins the game. We say two games are indistinguishable if no adversary can win one of the games with significantly larger probability than in the other.

Definition 4 (Game indistinguishability). Two CSLR $

π games g 1 and g 2 are game indistinguishable (written as g 1 ≈ g 2 ) if for every uniform CSLR $ adversary A of type Bits → Tτ , and every positive polynomial P , there exists some N ∈ N such that for all bitstrings η with |η| ≥ N ,

|Pr[ g 1 (η, A) 1] -Pr[ g 2 (η, A) 1]| < 1 P (|η|)
The above definition formalizes the idea that the change between the two games g 1 and g 2 cannot be noticed by an adversary.

Intuitively, the difference between computational indistinguishability and game indistinguishability is that, the former allows for any arbitrary use of the compared program by the adversary, while the latter provides more control over the adversary as it is usual in game-based security definitions, thus making game indistinguishability adequate. Hence, game indistinguishability is no stronger than computational indistinguishability as proved in the following proposition. This is why we can sometimes use the CSLR $ π proof system, which is designed for proving computational indistinguishability, for proving game indistinguishability.

Proposition 3. Computational indistinguishability in CSLR $

π implies game indistinguishability.

Proof. Let g 1 and g 2 be two arbitrary games of type Bits → ( Bits → Tτ ) → TBits. For every uniform CSLR $ adversary A of type Bits → Tτ , construct the following adversary A :

λη . λg . b $ ← g(η, A); if b ? = 1 then return(1) else return(0),
and it can be checked that A is still a uniform CSLR $ adversary and

Pr[ A (η, g i (η)) 1] = Pr[ g i (η, A) 1]. Because g 1 and g 2 are compu- tationally indistinguishable, |Pr[ A (η, g 1 (η)) 1] -Pr[ A (η, g 2 (η)) 1]| is negligible. 4.3. CSLR $ π proof system CSLR $
π inherits most of the equational proof system of CSLR: All the rules for program equivalence in CSLR can be used directly in CSLR $ π . No extra rules are needed for the primitive sample, but we can add rules for constants in π if necessary. The four rules for proving computational indistinguishability remain the same as in CSLR (Figure 2) except that in the rule SUB, a new premise enforces that the substitution context (the term e) must be a wellformed sampling program in CSLR $ , i.e., a program that uses sample properly and does not contain any superpolynomial-time constant.

ei : Bits → τ (i = 1, 2) e1 ≡+ e2 EQUIV e1 $ π e2 ei : Bits → τ (i = 1, 2, 3) e1 $ π e2 e2 $ π e3 TRANS-INDIST e1 $ π e3 x : n Bits, y : n τ e : τ ei : Bits → τ (i = 1, 2) e1 $ π e2 e is
The soundness of the system still holds and the proof just goes as for CSLR [START_REF] Zhang | The Computational SLR: a logic for reasoning about computational indistinguishability[END_REF]. In particular, the proof for the rule SUB contains a construction of a new adversary with the context, which remains a uniform CSLR $ adversary thanks to the new premise.

We will also use the program equivalence defined in [START_REF] Zhang | The Computational SLR: a logic for reasoning about computational indistinguishability[END_REF]. Roughly speaking, two terms e 1 and e 2 are equivalent (written e 1 ≡ e 2 ) if they have the same denotational semantics in any environment. Game transformation will consist in rewriting modulo the relation of game indistinguishability or computational indistinguishability or program equivalence. In particular, we will reuse as it is the equational proof system of [START_REF] Zhang | The Computational SLR: a logic for reasoning about computational indistinguishability[END_REF] for game transformations.

Note that the rule H-IND is not used throughout this paper, but it is an important rule representing the hybrid proof technique that is frequently used in cryptography. Interested readers can find more detailed explanations and examples in [START_REF] Zhang | The Computational SLR: a logic for reasoning about computational indistinguishability[END_REF].

Our further development in CSLR $ π also relies on a few intermediate lemmas that are frequently used in game-based proofs. The first one states that an expression e which does not depend on a random bit b cannot guess this bit b. Proof. We denote by e the program on the left-hand side. For every definable ρ ∈ Γ, e ρ = {(0, p 0 ), (1, p 1 )}, where

p 0 = Pr[ rand ρ = e ρ ] = 1 2 • Pr[ e ρ = 0] + 1 2 • Pr[ e ρ = 1] = 1 2 p 1 = Pr[ rand ρ = e ρ ] = 1 2 • Pr[ e ρ = 0] + 1 2 • Pr[ e ρ = 1] = 1 2
hence e ≡ rand.

The second lemma allows for a simplification when the semantics of a subexpression is a permutation. Remember that Z q is the set of bitstrings defined at the end of Section 3.1.

Lemma 4. Let f, f be two closed CSLR $ π terms of type Bits → Bits such that f is a permutation over B, and, for every bitstring q, f is a permutation over

{ f (v) | v ∈ Z q }. It holds that λη . x $ ← sample(q); return(f x) ≡ λη . x $ ← sample(q); return(f (f x))
Proof. Let e 1 , e 2 denote the two programs on the left-hand and right-hand side respectively. Then for a given bitstring η, e i (η) are two distributions over bitstrings, and dom( e

2 (η) ) = { f (v) | v ∈ Z q } = dom( e 1 (η) ) since f is a permutation over dom( e 1 (η) )
. Let e i be the program obtained from e i by replacing sample(q) with a fresh variable w, i.e., e i [sample(q)/w] = e i , then e i (η) = λw . e i (η) (Z $ q ). By Lemma 3.1 of [START_REF] Nowak | On formal verification of arithmetic-based cryptographic primitives[END_REF], e 1 (η) = λw . e 1 (η) (Z $ q ) = λw . e 2 (η) (Z $ q ) = e 2 (η) as f is a permutation.

Cryptographic constructions in CSLR $ π

This section presents examples of cryptographic constructions written in CSLR $ π . Note that they do not use any of the constants in π that are only to be used in the definitions of security notions.

The public-key encryption scheme ElGamal. Let G be a finite cyclic group of order q (depending on the security parameter η) and γ ∈ G be a generator. The ElGamal encryption scheme [START_REF]A public key cryptosystem and a signature scheme based on discrete logarithms[END_REF] can be implemented in CSLR $ π by the following programs:

• Key generation:

KG KG KG def = λη . x $ ← sample(q); return(γ x , x)
KG KG KG is of type Bits → T(Bits × Bits).

• Encryption:

Enc Enc Enc def = λη . λpk . λm . y $ ← sample(q); return(γ y , pk y * m) Enc Enc Enc is of type Bits → Bits → Bits → T(Bits × Bits).

• Decryption:

Dec Dec Dec def = λη . λsk . λc . proj 2 (c) * (proj 1 (c) sk ) -1
Dec Dec Dec is of type Bits → Bits → Bits → Bits, which does not involve monadic type because decryption is deterministic.

Note that when encoding cryptographic constructions in CSLR $ π , we put the security parameter η explicitly as the argument of the programs. However, as we work on bitstrings in CSLR $ π , the security parameter in traditional cryptographic contexts actually corresponds to |η| here. In the case of ElGamal encryption, the group order q will be determined by η. Particularly, for the encryption scheme to be semantically secure, we must choose a suitable group such that the DDH assumption holds, and its order will be necessarily exponential w.r.t. |η|. There are efficient algorithms that compute a suitable DDH group given η, hence can be programmed in CSLR $ π without using any constant from π [START_REF] Boneh | The Decision Diffie-Hellman problem[END_REF]. When sample is replaced by λx . zrand zrand zrand (x, η) in the functions KG KG KG, Enc Enc Enc, Dec Dec Dec, they are all computable in polynomial time w.r.t. η, even though Enc Enc Enc and Dec Dec Dec allow recursion on arguments other than η -these arguments (if valid) are all polynomially bound by η. Validity check of arguments are omitted in the implementation, but they can also be programmed in CSLR $ π without using any constant from π.

The Blum-Blum-Shub pseudorandom bit generator. The BBS generator defined in [START_REF] Blum | A simple unpredictable pseudo-random number generator[END_REF] is a deterministic function and can be programmed in CSLR $ π as follows:

BBS BBS BBS def = λη . λl . λs . bbsrec bbsrec bbsrec(η, l, s 2 mod n)

where bbsrec bbsrec bbsrec is defined recursively as bbsrec bbsrec bbsrec def = λη . λl . λx . if l ? = nil then nil else parity parity parity(x)•bbsrec bbsrec bbsrec(η, tail tail tail (l), x 2 mod n)

where n is determined by the security parameter η. BBS BBS BBS is a well-typed SLRfunction of type Bits → Bits → Bits → Bits, with the second argument being the length of the resulted pseudorandom bitstring and the third argument being the seed, which is polynomially bound w.r.t. η.

Security notions in CSLR $

π Security notions can be defined in term of game indistinguishability. We show how to use it to define some common security notions in cryptography.

Semantic security. A public-key encryption scheme (KG KG KG, Enc Enc Enc, Dec Dec Dec) is said to be semantically secure [START_REF] Goldwasser | Probabilistic encryption[END_REF] if: where A and A are of types, respectively, Bits → τ k → T(τ m × τ m × ( τ e → TBits)) and τ e → TBits. Note that τ k , τ e and τ m are the respective types of public keys, cipher-texts and plain-texts, which can be tuples of bitstrings that are distinguished in the language. Roughly speaking, it means that any adversary A playing the semantic security game (left-side game) cannot do significantly better than a random player (right-side game). The semantic security game is to be read as follows: A pair (pk, sk) of public and secret keys is generated; the public key pk is passed to the adversary A which returns two messages m 1 , m 2 and a function A , which can be seen as the continuation of the adversary A and contains necessary information that A has already obtained; one of the messages m b , is selected at random and encrypted with the public key pk; the obtained cipher-text c is then passed to the function A , which returns its guess b for the selected message; the result of the game indicates whether the adversary's guess is correct. where A is of type Bits → Bits → Bits. Roughly speaking, it means that any adversary A playing the unpredictability game (left-side game) cannot do significantly better than an adversary playing against a perfectly secure scheme (right-side game). The left-bit unpredictability game is to be read as follows: a seed s is selected at random in a set of cardinal q; the function F is then used to compute a pseudorandom bit sequence u of size l(|q|) > |q| where l is a polynomial; the sequence u minus its first bit is passed to the adversary A which returns its guess b for the first bit; the result of the game indicates whether the adversary's answer is correct. It was proved by Yao in [START_REF] Yao | Theory and applications of trapdoor functions[END_REF] that left-bit unpredictability is equivalent to passing all polynomial-time statistical tests.

A notion of next-bit unpredictability was defined in [START_REF] Zhang | The Computational SLR: a logic for reasoning about computational indistinguishability[END_REF], but it is based on the sampling from bitstrings of a given length. We can generalize this notion and obtain another notion of left-bit unpredictability, which we shall refer to as strong left-bit unpredictability because it implies the game-based notion of leftbit unpredictability [START_REF] Affeldt | Certifying assembly with formal cryptographic proofs: the case of BBS[END_REF]. An SLR-function F is strongly left-bit unpredictable Proof. The proof can be done using the CSLR $ π proof system. See Figure 3 for details.

Applications

Semantic security of the ElGamal encryption scheme

In this section, we illustrate our proof system by proving the semantic security of the ElGamal encryption scheme. The security of ElGamal is based on the the Decisional Diffie-Hellman (DDH) assumption [START_REF] Diffie | New directions in cryptography[END_REF], which can also be defined in CSLR $ π .

Decisional Diffie-Hellman assumption. Let q be a bitstring depending on the security parameter η, G be a finite cyclic group of order q and γ ∈ G be a generator. The Decisional Diffie-Hellman (DDH) assumption [START_REF] Diffie | New directions in cryptography[END_REF] states that, roughly speaking, no efficient algorithm can distinguish between triples of the form (γ x , γ y , γ xy ) and (γ x , γ y , γ z ) where x, y and z are random numbers such that 0 ≤ x, y, z < q. 3 It can be formalized in CSLR $ π as computational indistinguishability between two CSLR $ π programs: DDHL DDHL DDHL DDHR DDHR DDHR, where DDHL DDHL DDHL = λη . x $ ← sample(q); y $ ← sample(q); return(γ x , γ y , γ xy ) DDHR DDHR DDHR = λη . x $ ← sample(q); y $ ← sample(q); z $ ← sample(q); return(γ x , γ y , γ z ) Figure 4 shows the detailed proof of semantic security of the ElGamal encryption scheme, which follows the same structure as the one in [START_REF] Nowak | A framework for game-based security proofs[END_REF], but here the type system of CSLR guarantees that the adversary is probabilistic polynomialtime. This was not dealt with in [START_REF] Nowak | A framework for game-based security proofs[END_REF]. Moreover here all transformations are purely syntactic (thus allowing the immediate prospect of being implemented in an automated tool), while in [START_REF] Nowak | A framework for game-based security proofs[END_REF] they were done at the semantics level.

Note that by using Lemma 4, we assume that the adversary A will not send any junk messages, i.e., bitstrings that are not elements of the group G η . This is considered as a trivial case in cryptography proofs because the ElGamal encryption procedure will automatically reject the junk messages. But in practice, in more complex crypto-systems, this may not be trivial at all. In our proof system, we can also consider the case where adversaries may send junk messages. It suffices to provide the corresponding code in the program Enc Enc Enc which tests the validity of incoming messages, and we can still prove semantic security in the CSLR $ π proof system. Another possibility would be to use a richer type system to reject adversaries returning junk.

We also note that by replacing all occurence of sample(q) in the proof with zrand zrand zrand (q, η), we immediately obtain a proof for the semantic security of an implementation of the ElGamal scheme. The validity of the new proof is justified by Propositions 1 and 2.

Unpredictability of the BBS pseudorandom bit generator

CLSR+ also allows us to formalize directly the proof of unpredictability given in [START_REF] Nowak | On formal verification of arithmetic-based cryptographic primitives[END_REF] for the pseudorandom bit generator BBS. The proof requires a test for quadratic residuosity which is a superpolynomial-time computation -it can be introduced into CSLR $ π as a constant (in π). Moreover this proof is based on the Quadratic Residuosity Assumption stated below that uses arbitrary uniform choices.

Let n be a positive number and Z n be the set of integers modulo n. The multiplicative group of Z n is written Z * n and consists of the subset of integers modulo n which are coprime with n. An integer x ∈ Z * n is a quadratic residue modulo n iff there exists a y ∈ Z * n such that y 2 = x (mod n). Such a y is called a square root of x modulo n. We write Z * n (+1) for the subset of integers in Z * n with Jacobi symbol equal to 1.

Quadratic Residuosity Assumption. The quadratic residuosity problem is the following: given an odd composite integer n, decide whether or not an x ∈ Z * n (+1) is a quadratic residue modulo n. The quadratic residuosity assumption (QRA) states that the above problem is intractable when n is the product of two distinct odd primes [START_REF] Menezes | Handbook of Applied Cryptography[END_REF]. We reformulate the assumption in CSLR $ π :

λη . λA . x $ ← Z * n (+1) ; b $ ← A(η, n, x); return(b ? = qr qr qr (x)) ≈ λη . λA . rand
where A is of type Bits → Bits → Bits → TBits, qr qr qr (x) is the quadratic residuosity test of the element x of Z * n in our encoding, and n is a bitstring expression that depends on the security parameter η. Z * n (+1) is the CSLR $ implementation of the uniform distribution Z * n (+1), which can be defined using the uniform sampling primitive sample. The function qr qr qr is not definable in CSLR $ and is considered here as a native constant of type 4 Bits Bits in CSLR $ π . Also notice that the integer n, as well as elements in Z * n , are polynomially bounded by the security parameter η, so the adversary can safely make recursion over n and elements of Z * n without exceeding the complexity bound. This is often made implicit, sometimes unclear in traditional cryptographic proofs, and can lead to errors in proofs. CSLR $ makes it explicit by forcing the users to write well-typed terms that can be automatically type-checked.

The proof of left-bit unpredictability of BBS also relies on a set of numbertheoretic facts about Z * n and QR n (the set of quadratic residues modulo n). We list some of the facts that are necessary for building the proof, and their implications in terms of CSLR $ π programs. These facts (except the first one) assume that n is a Blum integer, which is the product of two distinct primes, both congruent to 3 modulo 4. In this case, each x ∈ QR n has a unique square root in QR n , which is called the principal square root and denoted by √ x. Note that in the sequel, we simply write x 2 (omitting the mod n part) for the group square operations in Z * n . Fact 1. The function which maps an x ∈ Z * n to x 2 ∈ QR n is a surjective 4-to-1 function. By Lemma 2, this implies that CSLR $ π is expressive enough to encode the proof of [START_REF] Nowak | On formal verification of arithmetic-based cryptographic primitives[END_REF] that BBS is left-bit unpredictable. where n is a Blum integer polynomially bound by the security parameter η and A is assumed to be a CSLR term of type Bits → Bits → Bits → TBits.

x $ ← Z * n ; return(x 2 ) ≡ QR n .
Proof. The proof is done in the proof system of CSLR $ π (cf. Figure 5).

Conclusions

We have extended Zhang's CSLR into CSLR $ π that provides a uniform framework to define cryptographic constructions, feasible adversaries, security notions, computational assumptions, game transformations, and game-based security proofs. CSLR $ π keeps the feature of characterizing PPT adversaries through typing in CSLR but allows users to write security games using a richer language, which is closer to the mathematical language and reduces the programming overhead.

As a future work, it might be interesting to allow arbitrary types in CSLR $ π because intermediate games might be easier to write without having to encode everything into bitstrings.

The most immediate direction for future work is to consider more complex examples. We could also consider an implementation of ElGamal that would use BBS as a source for pseudorandom bits. Another possible direction would be to implement CSLR $ π (possibly in a proof assistant) and develop a library of reusable security definitions, assumptions and game transformations. This would help dealing with complex examples.

The notion of oracle is frequently used in cryptography and it is sometimes necessary for defining security notions. For instance, with symmetric keys, an encryption oracle allows the adversary to encrypt messages without knowing the key. The higher-order nature of CSLR $ π makes it easy to define such oracles and it would be interesting to explore this direction.

← e 1 ;

 1 e 2 represents the probabilistic sequential computation bind x ← e 1 in e 2

Figure 1 :

 1 Figure 1: Some rules from the CSLR proof system

Proposition 1 .

 1 For any arbitrary s-sampling-based CSLR program P of type Bits → τ , with the sampling function variable s as the only free variable, λη . P (η)[λx . zrand zrand zrand (x, η)/s] λη . P (η)[sample/s].

Figure 2 :

 2 Figure 2: Rules for computational indistinguishability in CSLR $ π

Lemma 3 .

 3 If Γ e : TBits and, for all definable ρ ∈ Γ , the domain of the distribution e ρ is {0, 1}, then b $ ← rand; x $ ← e; return(x ? = b) ≡ rand where b ∈ dom(Γ).

←

  λη . λA . (pk, sk) $ ← KG KG KG(η); (m 0 , m 1 , A ) Enc Enc Enc(η, m b , pk); b $ ← A (c); return(b ? = b) ≈ λη . λA . rand

  Left-bit unpredictability. An SLR-function F is left-bit unpredictable if: λη . λA . s $ ← sample(q); u ← F (η, s); b $ ← A(η, tail tail tail (u)); return(b ? = head head head (u)) ≈ λη . λA . rand (1)

←

  sample(q); u ← F (η, s); b $ ← A(η, tail tail tail(u)); return(b ? = head head head(u)) η, tail tail tail(u)); return(b ? = head head head(u)) (By rules AX-BIND-3 and AX-BIND-1 of [36]) return(b •tail tail tail(F (η, s))) η, tail tail tail(u)); return(b ? = head head head(u)) (By strong left-bit unpredictability) ≡ λη . λA . s $ ← sample(q); b $ ← rand; u ← b •tail tail tail(F (η, s)); b $ ← A(η, tail tail tail(u)); return(b ? = head head head(u)) (By rules AX-BIND-3 and AX-BIND-1 of [36]) ≡ λη . λA . b $ ← rand; s $ ← sample(q); u ← b •tail tail tail(F (η, s)); b $ ← A(η, tail tail tail(u)); return(b ? = b ) (By rules AX-BIND-3 of [36]) ≡ λη . λA . rand (By Lemma 3)

Figure 3 :Proposition 4 .

 34 Figure 3: Proof of Proposition 4

Fact 2 .$←Fact 3 .Fact 4 .

 234 The function which maps an x ∈ QR n to x 2 ∈ QR n is a permutation. By Lemma 2, this implies that x QR n ; return(x 2 ) ≡ QR n . The function which maps an x ∈ Z * n (+1) to x 2 ∈ QR n is a surjective (2-to-1) function. By Lemma 2, this implies thatx $ ← Z * n (+1) ; return(x 2 ) ≡ QR n . For all x ∈ QR n , √ x 2 = x.Fact 5. For all x ∈ Z * n (+1), x ∈ QR n ⇔ parity parity parity(x) = parity parity parity( √ x 2 ).

Theorem 2 (

 2 Left-bit unpredictability of Blum-Blum-Shub PRG). For every positive integer l, λη . λA . s $ ← Z * n ; u ← BBS BBS BBS (η, l + 1, s); b $ ← A(η, n, tail tail tail (u)); return(b ? = head head head (u))≈ λη . λA . rand

;$←?; 1 ?= 1 ?=$v

 11 λη . λA . s $ ← Z * n ; u ← BBS BBS BBS(η, l + 1, s); b $ ← A(η, n, tail tail tail(u)); return(b ? = head head head(u)) ≡ λη . λA . s $ ← Z * n ; x ← s 2 ; u ← parity parity parity(x)•bbsrec bbsrec bbsrec(η, l, x 2 ); b $ ← A(η, n, tail tail tail(u)); return(b ? = head head head(u)) (Inline of the definition of BBS BBS BBS ) ≡ λη . λA . x b0 ← parity parity parity(x); v ← bbsrec bbsrec bbsrec(η, l, x 2 ); b $ ← A(η, n, v); return(b ? = b0) (By the equivalence rules AX-BIND-3 and AX-BIND-1 in [36]) ≡ λη . λA . x $ ← QR n; b0 ← parity parity parity(x); v ← bbsrec bbsrec bbsrec(η, l, x 2 ); b $ ← A(η, n, v); return(b ? = b0) (By Fact 1) ≡ λη . λA . x $ ← QR n; b0 ← parity parity parity( √ x 2 ); v ← bbsrec bbsrec bbsrec(η, l, x 2 ); b $ ← A(η, n, v); return(b ? = b0) (By Fact 4) ≡ λη . λA . y $ ← x QR n ; return(x 2 ) ; b0 ← parity parity parity( √ y); v ← bbsrec bbsrec bbsrec(η, l, y); b $ ← A(η, n, v); return(b ? = b0) (By the equivalence rules AX-BIND-3 and AX-BIND-1 in [36]) ≡ λη . λA . y $ ← QR n ; b0 ← parity parity parity( √ y); v ← bbsrec bbsrec bbsrec(η, l, y); b $ ← A(η, n, v); return(b b0 ← parity parity parity( √ y); v ← bbsrec bbsrec bbsrec(η, l, y); b $ ← A(η, n, v); return(b ? = b0) (By Fact 3.) ≡ λη . λA . z $ ← Z * n (+1) ; b0 ← parity parity parity( √ z 2 ); v ← bbsrec bbsrec bbsrec(η, l, z 2 ); b $ ← A(η, n, v); return(b ? = b0) (By the equivalence rules AX-BIND-3 and AX-BIND-1 in [36].) ≡ λη . λA . z $ ← Z * n (+1) ; v ← bbsrec bbsrec bbsrec(η, l, z 2 ); b $ ← A(η, n, v); return(b ⊕ parity parity parity(z) ⊕ parity parity parity( √ z 2 ) ⊕ parity parity parity(z) ⊕ 1) (By the equivalence rule AX-BIND-1 in [36], and apply function λx . x ⊕ parity parity parity(z) ⊕ 1 to both sides of equality test.) ≡ λη . λA . z $ ← Z * n (+1) ; v ← bbsrec bbsrec bbsrec(η, l, z 2 ); b $ ← A(η, n, v); return(b ⊕ parity parity parity(z) ⊕ qr qr qr(z)) (By Fact 5, where ⊕ is the notation of exclusive-or.) ≡ λη . λA . z ← bbsrec bbsrec bbsrec(η, l, z 2 ); b $ ← A(η, n, v); return(b ⊕ parity parity parity(z) ⊕ 1)   ; return(b ? = qr qr qr(z)) (By the equivalence rules AX-BIND-3 and AX-BIND-1 in [36].) ≈ λη . λA . rand (By QRA, considering the adversary λη . λn . λx .   v ← bbsrec bbsrec bbsrec(η, l, x 2 ); b $ ← A(η, n, v); return(b ⊕ parity parity parity(x) ⊕ 1)   , which is PPT by CSLR typing!)

Figure 5 :

 5 Figure 5: Proof of left-unpredictability of BBS

  e 1 e 2 | e 1 , e 2 | proj 1 e | proj 2 e | rand | return(e) | bind x ← e 1 in e 2B 0 and B 1 are two constants for constructing bitstrings: if u is a bitstring, B 0 u (respectively, B 1 u) is the new bitstring with a bit 0 (respectively, 1) added at the left end of u. case τ is the constant for case distinction: case τ (n, e, f 0 , f 1 ) tests the bitstring n and returns e if n is an empty bitstring, f 0 (n) if the first bit of n is 0 and f 1 (n) if the first bit of n is 1. rec τ is the constant for recursion on bitstrings: rec τ (e, f, n) returns e if n is empty, and f (n, rec τ (e, f, n ))

  e 1 ; e 2 represents the deterministic sequential (call-by-value) computation (λx . e 2 )e 1 ;

	• if e then e 1 else e 2 represents a simple case distinction
	case(e, e 2 , λ .e 2 , λ .e 1 ), which tests the first bit of e: if it is 1 then e 1 is
	executed, otherwise e 2 is executed;
	• when a program F is defined recursively by λn . rec τ (e 1 , e 2 , n), we often
	write the definition as:
		F	def = λn . if n	? = nil then e 1 else e 2 (n, F (tail tail tail (n))),
	where	?

  P by renaming each occurence of s by a distinct fresh variables s 1 , . . . , s n in P so that we have P [s/s 1 , . . . , s/s n ] = P ;

	1 1 , f 1 2 ), . . . , (f n 1 , f n 2 ) (n an arbitrary number), it holds that 1 (η)) λη . (f 1 1 (η), . . . , f n λη . (f 1 2 (η), . . . , f n 2 (η)).
	Next we define
	•

• Q by replacing each subterm s i (t i ) in P by a distinct fresh variable v i , i.e., Q [s 1 (t 1 )/v 1 , . . . , s n (t n )/v n ] = P (it is clear that each t i has either no free variable or only η as a free variable);

  Bits, n : n Bits e : τ λn.e[u/x] is numerical for all bitstrings u λx . e[i(x)/n] $ π λx . e[B1i(x)/n] for all canonical polynomials i such that |i| < |p|

	well-formed sampling program in CSLR $	SUB
	λx . e[e1(x)/y] x : n H-IND $ π λx . e[e2(x)/y]
	λx . e[nil/n]	$ π λx . e[p(x)/n]

Another possible approach is to select a random value in a very large distribution, and then take the remainder modulo the cardinal of the desired distribution.

We do not assume that q is prime. However most groups in which DDH is believed to be true have prime order[START_REF] Boneh | The Decision Diffie-Hellman problem[END_REF].

The type of qr qr qr is defined as a linear function type so that it can take linear arguments.

Acknowledgements

We would like to thank the reviewers for their comments and suggestions that helped to improve significantly this paper.