Manuel Barbosa

Benjamin Grégoire
email: benjamin.gregoire@inria.fr

Gilles Barthe
email: gbarthe@mpi-sp.org

Mechanized Proofs of Adversarial Complexity and Application to Universal Composability

Keywords: CCS Concepts:, Theory of computation → Interactive proof systems, • Security and privacy → Logic and verification Verification of Cryptographic Primitives, Formal Methods, Interactive Proof System, Complexity Analysis

In this paper we enhance the EasyCrypt proof assistant to reason about computational complexity of adversaries. The key technical tool is a Hoare logic for reasoning about computational complexity (execution time and oracle calls) of adversarial computations. Our Hoare logic is built on top of the module system used by EasyCrypt for modeling adversaries. We prove that our logic is sound w.r.t. the semantics of EasyCrypt programs -we also provide full semantics for the EasyCrypt module system, which was previously lacking.

We showcase (for the first time in EasyCrypt and in other computer-aided cryptographic tools) how our approach can express precise relationships between the probability of adversarial success and their execution time. In particular, we can quantify existentially over adversaries in a complexity class, and express general composition statements in simulation-based frameworks. Moreover, such statements can be composed to derive standard concrete security bounds for cryptographic constructions whose security is proved in a modular way. As a main benefit of our approach, we revisit security proofs of some well-known cryptographic constructions and we present a new formalization of Universal Composability (UC).

INTRODUCTION

Cryptographic designs are typically supported by mathematical proofs of security. Unfortunately, these proofs are error-prone and subtle flaws can go unnoticed for many years, in spite of careful and extensive scrutiny from experts. Therefore, it is desirable that cryptographic proofs are formally verified using computer-aided tools [START_REF] Halevi | A plausible approach to computer-aided cryptographic proofs[END_REF]. Over the last decades, many formalisms and tools have been developed for mechanizing cryptographic proofs [START_REF] Barbosa | SoK: Computer-Aided Cryptography[END_REF]. In this paper we focus on the EasyCrypt proof assistant [START_REF] Barthe | EasyCrypt: A Tutorial[END_REF][START_REF] Barthe | Computer-Aided Security Proofs for the Working Cryptographer[END_REF], which has been used to prove security of a diverse set of cryptographic constructions in the computational model of cryptography [START_REF] Almeida | A Machine-Checked Proof of Security for AWS Key Management Service[END_REF][START_REF] Bacelar Almeida | Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3[END_REF]. In this setting, cryptographic designs and their corresponding security notions are modeled as probabilistic programs. Moreover, security proofs provide an upper bound on the probability that an adversary breaks a cryptographic design, often assuming that the attacker has limited resources that are insufficient to solve a mathematical problem. While EasyCrypt excels at quantifying the probability of adversarial success, it lacks support for keeping track of the complexity of adversarial computations. This is a limitation that is common to other tools in computer-aided cryptography, and it means that manual inspection is required to check that the formalized claims refer to probabilistic programs that fall in the correct complexity classes. While this may be acceptable for very simple constructions, for more intricate proofs it may be difficult to interpret what a proved claim means in the cryptographic sense; in particular, existing computer-aided tools cannot fully express the subtleties that arise in compositional approaches such as Universal Composability [START_REF] Canetti | Universally Composable Security: A New Paradigm for Cryptographic Protocols[END_REF]. This is an important limitation, as compositional approaches are ideally suited for proving security of complex cryptographic designs involving many layers of simpler building blocks. This work overcomes this limitation and showcases the benefits of reasoning about computational complexity in EasyCrypt, through three broad contributions.

Formal verification of complexity statements. We define a formal system for specifying and proving complexity claims. Our formal system is based on an expressive module system, which enriches the existing EasyCrypt module system with declarations of memory footprints (specifying what is read and written) and cost (specifying which oracles can be called and how often). This richer module system is the basis for modeling the cost of a program as a tuple. The first component of the tuple represents the intrinsic cost of the program, i.e. its cost in a model where oracle and adversary calls are free. The remaining components of the tuple represent the number of calls to oracles and adversaries. This style of modeling is compatible with cryptographic practice and supports reasoning compositionally about (open) programs.

Our formal system is built on top of the module system and takes the form of a Hoare logic for proving complexity claims that upper bound the cost of expressions and commands. Furthermore, an embedding of the formal system into a higher-order logic provides support for reductionist statements relating adversarial advantage and execution cost, for instance: ∀A.∃B. adv S (A) ≤ adv H (B) + ϵ ∧ cost(B) ≤ cost(A) + δ where typically ϵ and δ are polynomial expressions in the number of oracle calls. The above statement says that every adversary A can be turned into an adversary B, with sensibly equivalent resources, such that the advantage of A against a cryptographic scheme S is upper bounded by the advantage of B against a hardness assumption H . Note that the statement is only meaningful because the cost of B is conditioned on the cost of A, as the advantage of an unbounded adversary is typically large (e.g., it succeeds with probability 1). The ability to prove and instantiate such ∀∃-statements is essential for capturing compositional reasoning principles. We show correctness of our formal system w.r.t. an interpretation of programs. Our interpretation provides the first complete semantics for the EasyCrypt module system, which was previously lacking. This semantics is of independent interest and could be used to prove soundness of the two program logics supported by EasyCrypt: a Relational Hoare Logic [START_REF] Barthe | Formal certification of code-based cryptographic proofs[END_REF] and a Union Bound logic [START_REF] Barthe | A Program Logic for Union Bounds[END_REF].

Implementation in the EasyCrypt proof assistant. We have implemented our formal system as an extension to the EasyCrypt proof assistant, which provides mechanisms for declaring the cost of operators and for helping users derive the cost of expressions and programs. Our implementation brings several contributions of independent interest, including an improvement of the memory restriction system of EasyCrypt, and a library and automation support to reason about extended integers that are used for reasoning about cost. For the latter we follow [START_REF] Sharma | Certified Reasoning with Infinity[END_REF] and reduce formulae about extended integers to integer formulae that can be sent to SMT solvers. Another key step is to embed our Hoare logic for cost into the ambient higher-order logic-similar to what is done for the other program logics of EasyCrypt. This allows us to combine judgments from different program logics, and it enhances the expressiveness of the approach. Implementation-wise, this extension required to add or rewrite around 8 kLoC of EasyCrypt. The implementation and examples (including those of the paper as well as classic examples from the EasyCrypt distribution, including Bellare and Rogaway BR93 Encryption, Hashed ElGamal encryption, Cramer-Shoup encryption, and hybrid arguments) are open source [START_REF]Source code of our EasyCrypt[END_REF].

Case study: Universal Composability. Universal Composability [START_REF] Canetti | Universally Composable Security: A New Paradigm for Cryptographic Protocols[END_REF][START_REF] Canetti | Universally composable security: a new paradigm for cryptographic protocols[END_REF] (UC) is a popular framework for reasoning about cryptographic systems. Its central notion, called UC-emulation, formalizes when a protocol π 1 can safely replace a protocol π 2 . Informally, UC-emulation imposes that there exists a simulator S capable of fooling any environment Z by presenting to it a view that is fully consistent with an interaction with π 1 , while it is in fact interacting with S(π 2 ). This intuition, however, must be formalized with tight control over the capabilities of the environment and the simulator. If this were not the case, the definition would make no sense: existential quantification over unrestricted simulators is too weak (it is crucial for the compositional security semantics that simulators use comparable resources to real-world attackers), whereas universal quantification over unrestricted environments results in a definition that is too strong to be satisfied [START_REF] Canetti | Universally Composable Security: A New Paradigm for Cryptographic Protocols[END_REF][START_REF] Canetti | Universally Composable Security: A New Paradigm for Cryptographic Protocols[END_REF]. Moreover, when writing proofs in the UC setting, it is often necessary to consider the joint resources of a sub-part of a complex system that involves a mixture of concrete probabilistic algorithms and abstract adversarial entities, when they are grouped together to build an attacker for a reductionistic proof. In these cases, it is very hard to determine by inspection whether the constructed adversaries are within the complexity classes for which the underlying computational assumptions are assumed to hold. Therefore, tool support for complexity claims is of particular importance with UC -conversely, UC is a particularly challenging example for complexity claims.

Using our enriched implementation of EasyCrypt, we develop a new fully mechanized formalization of UC. In contrast to [START_REF] Canetti | EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security[END_REF], which chooses to follow closely the classic execution model for UC, our mechanization adopts a more EasyCrypt-friendly approach that is closer to the simplified version of UC proposed by Canetti, Cohen and Lindell in [START_REF] Canetti | A Simpler Variant of Universally Composable Security for Standard Multiparty Computation[END_REF]; this is further discussed in Section 6. Our mechanization covers the core notions of UC, the classic composition lemmas, transitivity and composability, which respectively state that UC-emulation (as a binary relation between cryptographic systems) is closed under transitivity and arbitrary adversarial contexts. More importantly, our development captures for the first time the complexity aspects of these general results. As an illustrative application of our approach we revisit the example used in [START_REF] Canetti | EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security[END_REF], where modular proofs for Diffie-Hellman key exchange and encryption over ideal authenticated channels are composed to construct a UC secure channel.

Discussion. The possibility to quantify over adversary using complexity claims introduces conceptual simplifications in layered proofs by i. supporting compositional reasoning and ii. avoiding the use of explicit cost accounting modeling. The downside is that it also introduces some additional burden on users, who now must prove complexity claims. However, we note that our extension does not invalidate existing Easycrypt developments: complexity claims are optional, existing proofs have been left unchanged, and their type-checking remains as fast as before. Furthermore, it is possible to layer the complexity claims on top of standard EasyCrypt proofs that do not capture the complexity aspects -in effect, this is what we did in our example. We have also provided rudimentary support to automate proofs of complexity claims, and could enhance this support even further by adopting ideas from cost analysis. We think that the current tool is significantly more usable and scalable than prior versions without support for complexity reasoning.

To make this claim more concrete, let us consider the implications of refactoring an existing EasyCrypt development and extend it to take advantage of cost analysis for both dealing with query counts and to include complexity claims. Removing the layer of modular wrapping that explicitly keeps track of query counts leads to more readable code, and has essentially no impact on the proofs. However, when it comes to complexity claims, new specifications and proof scripts must be added to the development. The new specifications consist of the description of the cost model and the declarations of the types of the various algorithms, which include explicit cost expressions. The additional proof effort consists of applying our logic to prove complexity claims and discharging the relevant side-conditions. As a coarse metric on the additional proof and specification efforts required, we consider the ratio of the number of lines of codes related to the cost analysis over the total number of lines. For the example presented in the next section, this ratio is 117/495. For the Universal Composability example, the ratio is 270/2300 for the concrete protocol and 791/1775 for the general composition theorems. We also note that there is a large body of work on automated complexity analysis, as mentioned in the related work section, which might reduce this overhead.

This paper is an extended version of [START_REF] Barbosa | Mechanized Proofs of Adversarial Complexity and Application to Universal Composability[END_REF], which was presented at the ACM CCS'21 conference. Modules are a key ingredient of an EasyCrypt formalization. Roughly, a module is a structure packaging together variable and procedures declarations. Modules can be parameterized by one or more modules -such parameterized modules are called functors. Fig. 1 gives a small example of a functor named BR93 implementing the BR93 encryption function. This module is parameterized by a module H modeling the random oracle used by the encryption scheme, which it uses in its implementation of the enc procedure. Modules types are used to structure module declarations, by declaring the signature of the procedures that must be included in a module. Coming back to our example, RO is a module type stating that H must declare a procedure named o from values of type rand to values of type plaintext (c.f. Fig. 2) -the type of values outputted by the encryption. Finally, a module can contains sub-modules, allowing for a rich hierarchical presentation.

Intuitively, the RO is used to convert the message into a random input for the trapdoor permutation so as to allow a reduction to the one-wayness property. This proof strategy is used in BR93 and many other schemes, including OAEP [START_REF] Bellare | Random Oracles are Practical: A Paradigm for Designing Efficient Protocols[END_REF]. Fig. 2 shows the code of an inverter for the trapdoor permutation that is constructed from an attacker against the encryption scheme. 1 This inverter simulates the single random oracle used by the encryption scheme for the attacker and recovers the pre-image to y with essentially the same probability as the attacker breaks the encryption scheme.

We first define module types for random oracles RO, schemes Scheme, and adversaries Adv. The module type for random oracles declares a single procedure o with cost ≤ t o . The module type for schemes declares three procedures for key generation, encryption, and decryption, and is parameterized by a random oracle H. No cost declaration is necessary. The module type for (chosenplaintext) adversaries declares two procedures: choose for choosing two plaintexts m 0 and m 1 , and guess for guessing the (uniformly sampled) bit b given an encryption of m b . The cost of these procedures is a pair: the second component is an upper bound on the number of times it can call the random oracle, and the first is an upper bound on its intrinsic cost, i.e. its cost assuming that oracle calls (modeled as functor parameters) have a cost of 0. This style of modeling is routinely used in cryptography and is better suited to reason about open code. This cost model is also more fine-grained than counting the total cost of the procedure including the cost of the oracles, as we have a guarantee on the number of time oracles are called.

Next, we define the inverter Inv for the one-way trapdoor permutation. It runs the adversary A, keeping track of all the calls that A makes to H in a list qs (using the sub-module QH), and then searches in the list qs for a pre-image of y under f pk. Search is done through a while loop, which we write in a slightly beautified syntax. This inverter can be used to state the following reductionist security theorem relating the advantage and execution cost of an adversary against chosen-plaintext security of the PKE with the advantage of the inverter against one-wayness. Theorem 2.1 (Security of BR93). Let t f represent the cost of applying the one-way function f and t o denote the cost of H.o, i.e. the implementation of a query to a lazily sampled random oracle. Fix the type for adversaries τ A such that:

cost A.choose ≤ compl[intr : t c , H.o : k c ] and cost A.guess ≤ compl[intr : t д , H.o : k д ]
and fix τ I such that:

cost I.invert ≤ compl[intr : (5 + t f ) • (k c + k д ) + 4 + t o • (k c + k д ) + t c + t д ] . Then, ∀A ∈ τ A , ∃I ∈ τ I , adv BR93 ind-cpa (A) ≤ adv f ow (I).
Here, IND-CPA refers to the standard notion of ciphertext indistinguishability under chosenplaintext attacks for PKE, where the adversary is given the public key and asked to guess which of two messages of its choice has been encrypted in a challenge ciphertext; OW refers to the standard one-wayness definition for trapdoor permutations, where the attacker is given the public parameters and the image of a random pre-image, which it must invert. In the former, advantage is the absolute bias of the adversary's boolean output w.r.t. 1/2; in the latter, advantage is the probability of successful inversion.

We prove the statement by providing Inv(A) as a witness for the existential quantification, which creates two sub-goals. The first sub-goal establishes the advantage bound, which we prove using relational Hoare logic. The second sub-goal establishes that our inverter satisfies the required cost restrictions, and is proved using our Hoare logic for complexity. We declare the type of Inv as:

cost Inv.invert ≤ compl[intr : (5 + t f ) • (k c + k д ) + 4, H.o = k c + k д , A.choose = 1, A.дuess = 1]
and so we first must establish that Inv belongs to this functor type. It is easy to show that A.choose and A.guess are called exactly once, and that H.o is called at most k c + k д times. So we turn to the intrinsic complexity of Inv. The key step for this proof is to show that the loop does at most k c + k д iterations. We use the length of qs as a variant: the length of the list is initially 0, and incremented by 1 by each call to the random oracle, therefore its length at the start of the loop is at most k c + k д . Moreover, the length decreases by 1 at each iteration, so we are done. The remaining reasoning is standard, 2 using the cost of each operator-fixed by choice in this particular example to 1, except for the operator f. Our modeling of cost enforces useful invariants that simplify reasoning. For instance, proving upper bounds on the execution cost of Inv requires proving an upper bound on the number of iterations of the loop, and therefore on the length of qs upon entering the loop. We derive the complexity statement in the theorem, which shows only the intrinsic cost of Inv, by instantiating the complexity type of Inv with the cost of its module parameter A. This illustrates how our finer-grained notion of cost is useful for compositional reasoning.

Comparison with EasyCrypt. Our formalization follows the same pattern as the BR93 formalization from the EasyCrypt library. However, the classic module system of EasyCrypt only tracks read-andwrite effects and lacks first-class support for bounding the number of oracle calls and for reasoning about the complexity of programs. To compensate for this first point, classic EasyCrypt proofs use wrappers to explicitly count the number of calls and to return dummy answers when the number of adversarial calls to an oracle exceeds a threshold. The use of wrappers suffices for reasoning Expressions (distribution expressions are similar):

e ::= v ∈ V (variable) | f (e 1 , . . . , e n ) (if f ∈ F E )
Statements: Module declarations: about adversarial advantage. However, no similar solution can be used for reasoning about the computational cost of adversaries. Therefore, the BR93 formalization from the EasyCrypt library makes use of the explicit definition of I, and users must analyze the complexity of I outside the tool. As a result, machine-checked security statements are partial (complexity analysis is missing), cluttered (existential quantification is replaced by explicit witnesses), and compositional reasoning is hard (existential quantification over module types cannot be used meaningfully).

s ::= abort (abort) | skip (skip) | s 1 ; s 2 (sequence) | x ← e (assignment) | x $ ← -d (sampling) | x ← call F(ì e ) (proc. call) | if e then
d ::= module x = m | proc f ( ì v : ì τ ) → τ r = body

ENRICHED EASYCRYPT MODULE SYSTEM

We present a formalization of our extended module system for EasyCrypt. It is based on EasyCrypt current imperative probabilistic programming language and module system, which we enrich to track the read-and-write memory footprint and complexity cost of module components through module restrictions. These module restrictions are checked through a type system: memory footprint type-checking is fully automatic, while type-checking a complexity restriction generates a proof obligation that is discharged to the user -using the cost Hoare logic we present later, in Section 4.

Syntax of Programs and Modules

The syntax of our language and module system is (quite) standard and summarized in Fig. 3. We describe it in more detail below. We assume given a set of operators F E and a set of distribution operators F D . For any д ∈ F E ∪ F D , we assume given its type: type(д) = τ 1 × • • • × τ n → τ where τ 1 , . . . , τ n , τ ∈ B with B the set of base types. We require that bool is a base type, and otherwise leave B unspecified.

We consider well-typed arity-respecting expressions built from F E and variables in V. Similarly, distribution expressions d are built upon F D and V. For any expression e, we let vars(e) be the set of variables appearing in e (idem for distribution expression). Module restrictions:

θ ::= ϵ | θ, (f : λ) λ ::= ⊤ | λ m ∧ λ c
Memory restrictions (for any l ∈ N):

λ m ::= +all mem\{v 1 , . . . , v l } | {v 1 , . . . , v l }
Complexity restrictions (for any l, k, k 1 , . . . , k l ∈ N): We assume a simple language for program statements. A statement s can be an abort, a skip, a statement sequence s 1 ; s 2 , an assignment x ← e of an expression to a variable, a random sampling x $ ←d from a distribution expression, a conditional, a while loop, or a procedure call x ← call F(ì e ).

λ c ::= ⊤ | compl[intr : k, x 1 .f 1 : k 1 , . . . , x l .f l : k l ]
The module system. In a procedure call, F is a function path of the form p.f where f is the procedure name and p is a module path. Basically, when calling p.f , the module system will resolve p to a module structure, which must declare the procedure f (this will be guaranteed by our type system). Formally, a module structure st is a list of module declarations, and a module declaration d is either a procedure (with typed arguments, and a body which comprises a list of local variables with their types ì v : ì τ , a statement s and a return expression e) or a sub-module declaration. The component c of a module x can be accessed through the module path expression x.c. Since a module can contain sub-modules, we can have nested accesses, as in x. . . . .z.c. Hence, a module path is either a module identifier, a component access of another module path p, or a functor application. Finally, a module expression m is either a module path, a module structure or a functor.

Module Signatures and Restrictions

The novel part of our system is the use of module restrictions in module signatures. Objects related to module restriction are highlighted in red throughout this paper (this is only here to improve readability, not to convey additional information). The syntax of module signatures and restrictions is given in Fig. 4. A module structure signature S is a list of module signature declarations, which are procedure signatures or sub-module signatures. Then, a module signature M is either a functor signature, or a structure signature with a module restriction θ attached.

Module restrictions. A module restriction restricts the effects of a module's procedures. We are interested in two types of effects. First, we characterize the memory footprint (i.e. global variables which are read or written to) of a module's procedures through memory restrictions. Second, we upper bound the execution cost of a procedure, and the number of calls a functor's procedure can make to the functor's parameters, through complexity restrictions.

Restrictions are useful for compositional reasoning, as they allow stating and verifying properties of a module's procedures at declaration time. In the case of an abstract module (i.e. a module whose code is unknown), restrictions allow to constrain, through the type system, its possible instantiations. This is a key idea of our approach, which we exploit to prove complexity properties of cryptographic reductions. For example, we give in Fig. 5 EasyCrypt code corresponding to an adversary against a hardware security module. In this scenario the goal of the adversary is to recover the secret key stored in the module Hsm. The example uses two types of restrictions. The module-level restriction {+all mem, -Hsm} states that such an adversary can access all the memory, except for the memory used by the module Hsm. The procedure-level restriction [intr : k 0 , H.enc : k] attached to guess, states that guess execution time is at most k 0 (excluding calls to H.enc), and that guess can make at most k queries to the procedure H.enc.

Formally, a module restriction is a list of pairs comprising a procedure identifier f and a procedure restriction λ, and a procedure restriction λ is either ⊤ (no restriction), or the conjunction of a memory restriction λ m and a complexity restriction λ c : Memory. A memory restriction λ m , attached to a procedure f , restricts the variables that f can access directly. We allow for positive memory restrictions {v 1 , . . . , v l }, which states that f can only access the variables v 1 , . . . , v l ; and negative memory restrictions +all mem\{v 1 , . . . , v l }, which states that f can access any global variables except the variables v 1 , . . . , v l .

Note that λ m only restricts f 's direct memory accesses: this excludes the memory accessed by the procedure oracles (which are modeled as functor's parameters). This is crucial, as otherwise, an adversary that is not allowed to access some oracle's memory (a standard assumption in security proofs) would not be allowed to call this oracle. E.g., the adversary of Fig. 5 can call the oracle H.enc (which can be instantiated by Hsm), even though it cannot access directly Hsm's memory.

Complexity. A complexity restriction λ c attached to a procedure f restricts its execution time and the number of calls that f can make to its parameters: it is either ⊤, i.e. no restriction; or the restriction compl[intr : k, x 1 .f 1 : k 1 , . . . , x l .f l : k l ], which states that: i) its execution time (excluding calls to the parameters) must be at most k; ii) f can call, for every i, the parameter's procedure x i .f i at most k i times. We require that all parameters' procedures appear in the restriction. This can be done w.l.o.g. by assuming that any missing entry is zero (which is exactly what is done in our EasyCrypt implementation). We now present the core rules of our module type system, which are summarized in Fig. 6 and Fig. 8. The rest of the rules are postponed to Appendix A. For clarity of presentation, our module type system requires module paths to always be long modules paths, from the root of the program to the sub-module called (we give a simple example in Fig. 7). This allows to have a simpler module resolution mechanism, by removing any scoping issues. This is done without loss of Module path typing Γ ⊢ p : M.

Typing Enriched Module Restrictions

Name

Γ(p) = _ : M Γ ⊢ p : M Compnt Γ ⊢ p : sig S 1 ; module x : M; S 2 restr θ end Γ ⊢ p.x : M FuncApp Γ ⊢ p : func(x : M ′ ) M Γ ⊢ p ′ : M ′ Γ ⊢ p(p ′ ) : M[x → mem Γ (p ′ )]
Module expression typing Γ ⊢ p m : M. We omit the rules Γ ⊢ M to check that a module signature M is well-formed.

Alias

Γ ⊢ p a : M Γ ⊢ p p a : M Struct Γ ⊢ p,θ st : S Γ ⊢ p struct st end : sig S restr θ end Func Γ ⊢ M 0 Γ(x) undef Γ, module x = abs param : M 0 ⊢ p(x) m : M Γ ⊢ p func(x : M 0 ) m : func(x : M 0 ) M Sub Γ ⊢ p m : M 0 ⊢ M 0 <: M Γ ⊢ p m : M Module structure typing Γ ⊢ p,θ st : S. ProcDecl body = { var ( ì v l : ì τ l ); s; return r } ì v, ì v l fresh in Γ Γ f = Γ, var ì v : ì τ , var ì v l : ì τ l Γ f ⊢ s Γ f ⊢ r : τ r Γ ⊢ body ▷ θ [f ] Γ(p.f ) undef Γ, proc p.f ( ì v : ì τ ) → τ r = body ⊢ p,θ st : S Γ ⊢ p,θ (proc f ( ì v : ì τ ) → τ r = body; st) : (proc f ( ì v : ì τ ) → τ r ; S) ModDecl Γ ⊢ p.x m : M Γ(p.x) undef Γ, module p.x = m : M ⊢ p,θ st : S Γ ⊢ p, θ (module x = m; st) : (module x : M; S) StructEmp Γ ⊢ p, θ ϵ : ϵ Environments typing ⊢ E EnvEmp ⊢ ϵ EnvSeq ⊢ E E ⊢ δ ⊢ E, δ EnvVar E(v) undef E ⊢ var v : τ EnvMod E ⊢ x m : M E(x) undef E ⊢ (module x = m : M) EnvAbs E ⊢ M l E(x) undef E ⊢ (module x = abs K : M)
Fig. 6. Core typing rules.

generality: in practice, one can always replace short module paths with long module paths when parsing a program. A typing environment Γ is a list of typing declarations. A typing declaration, denoted δ , is either a variable, module, abstract module or procedure declaration, with a type.

δ ::= var v : τ | module p = m : M | module x = abs K : M | proc p.f ( ì v : ì τ ) → τ r = body K ::= open | param Γ ::= ϵ | Γ, δ
Note that module and procedure declarations can be rooted at an arbitrary path p.

An abstract module declaration module x = abs K : M states that x is a module with signature M whose code is unknown. This is used either for open code, or to represent a functor parameter at typing time. Open modules and parameters are treated differently by the type system: a memory restriction ignores the memory footprint of a functor parameter; and a complexity restriction restricts the number of calls that can be made by parameters' procedures. Therefore, we annotate an abstract module with its kind, which can be open or param. Finally, module and procedure declarations come with the absolute path from the root of the program to the parent module where the declaration is made (variable and abstract modules are always declared at top-level).

For example, the entry (module p.x = m : M) means that there is a sub-module m named x and with type M declared at path p. As usual we require that typing environments do not contain two declarations with the same path. This allows to see a typing environment Γ as a partial function from variable names v, module paths p or procedure paths p.f to (base, module, abstract modules or procedure) values and their types, defined as follows:

Γ(v) = τ ( if Γ = (Γ 1 ; var v : τ ; Γ 2 )) 1:11 Γ(p) = m : M ( if Γ = (Γ 1 ; module p = m : M; Γ 2 )) Γ(x) = abs K x : M ( if Γ = (Γ 1 ; module x = abs K : M; Γ 2 )) Γ(p.f ) = proc f ( ì v : ì τ ) → τ r = body ( if Γ = (Γ 1 ; proc p.f ( ì v : ì τ ) → τ r = body; Γ 2 ))
and Γ(z) = undef otherwise. Also, we write Γ(z) undef when Γ(z ′ ) = undef. for any prefix z ′ of z.

= proc f ( ì v : ì τ ) → τ r
Basically, we only allow module structures, or functors whose parameters are module structures. This restriction is motivated by the fact that further generality is not necessary for cryptographic proofs (adversaries and simulations usually return base values, not procedures); and, more importantly, this restriction allows the abstract call rule of our instrumented Hoare logic Abs presented in Fig. 12 to remain tractable.

For any M l , we let procs(M l ) = { f 1 , . . . , f n } be the set of procedure names declared in M l .

Environments. The semantics of programs, presented later in Section 5, is parametrized by an environment E. Essentially, a environment is a typing environment that do not contain abstract module declarations of kind, and which contains only top-level module declaration (i.e. with a module path of the form x).

E ::= ϵ | E, var v : τ | E, module x = m : M | E, module x = abs open : M l
For any E, we let abs(E) = {x 1 , . . . , x n } be the set of abstract module names declared in E.

Typing module paths. The typing judgment Γ ⊢ p : M states that the module path p refers to a module with type M. Its typing rules, which are given in Fig. 6, are standard [START_REF] Leroy | Applicative Functors and Fully Transparent Higher-Order Modules[END_REF], except for the functor application typing rule FuncApp:

FuncApp Γ ⊢ p : func(x : M ′ ) M Γ ⊢ p ′ : M ′ Γ ⊢ p(p ′ ) : M[x → mem Γ (p ′ )]
A key point here is that we need to substitute x in the module signature. The substitution function is standard (see Fig. 24), except for module restrictions, which are modified as follows:

• a memory restriction restricts the variables that a procedure can access directly -however, memory accesses done through functor parameters are purposely not restricted. Hence, when we instantiate a functor parameter x by a module path p ′ , we must add its memory footprint, which is mem Γ (p ′ ). This is handled when substituting x in a memory restriction:

λ m [x → mem Γ (p ′ )] = λ m ⊔ mem Γ (p ′ )
• a complexity restriction gives upper bounds on a procedure execution time, and on the number of calls it can make to its functors' parameters. When we instantiate a functor, we remove a functor parameter, and therefore remove the corresponding entries in the

Restriction checking Γ ⊢ { var ( ì v l : ì τ l ); s; return e } ▷ θ . RestrCheck Γ ⊢ body ▷ λ m Γ ⊢ body ▷ λ c Γ ⊢ body ▷ λ m ∧ λ c RestrMem Γ ⊢ s ▷ λ m Γ ⊢ e ▷ λ m Γ ⊢ { _; s; return e } ▷ λ m RestrMemS mem Γ (s) ⊑ λ m Γ ⊢ s ▷ λ m RestrMemE vars(e) ⊑ λ m Γ ⊢ e ▷ λ m RestrComplTop Γ ⊢ body ▷ ⊤ RestrCompl E ⊢ {⊤} s {ψ | t } ⊢ {ψ } r ≤ t r (t + t r • 1 conc ) ≤ compl λ c E ⊢ { _; s; return r } ▷ λ c
Notes: the relation ⊑ checks the inclusion of a memory restriction into another, and is defined in Fig. 22. Also, mem Γ (s) computes an over-approximation of a instruction's memory footprint, and is defined in Fig. 23. complexity restrictions.

compl[intr : k, y 1 .f 1 : k 1 , . . . , y l .f l : k l ][x → _] = compl[intr : k, (y 1 .f 1 : k 1 )[x → _], . . . , (y l .f l : k l )[x → _]]
where

(y.f : k)[x → _] = ϵ if y = x y.f : k otherwise
Also, note that when substituting x into p in p.y, we do not substitute the module component identifier y (essentially, only top-level module names are substituted). Similarly, when we substitute x into p in a module declaration (module y = m), we ignore y.

Other typing rules. The typing judgment for module expressions Γ ⊢ p m : M states that the module expression m, declared at path p, has type M. Functor are typed by the Func rule. Note that the functor body is typed in an extended typing environment, where the module parameter x has been declared as an abstract module with kind param.

The typing judgment for module structures Γ ⊢ p,θ st : S is annotated by both the module path of the structure being typed, and the module restriction θ that the structure must verify. Remark that when we type a procedure using ProcDecl, we check that the procedure f body satisfies the module restriction θ [f ] by requiring that the restriction checking judgment Γ ⊢ body ▷ θ [f ] holds.

Restrictions. The restriction checking rules are given in Fig. 8. The RestrMem rule checks that a procedure body { _; s; return e } (where s is the procedure's instructions, and e the returned expression) verifies a memory restriction through a fully automatic syntactic check done in the auxiliary rules RestrMemS and RestrMemE.

RestrMem Γ ⊢ s ▷ λ m Γ ⊢ e ▷ λ m Γ ⊢ { _; s; return e } ▷ λ m RestrMemS mem Γ (s) ⊑ λ m Γ ⊢ s ▷ λ m RestrMemE vars(e) ⊑ λ m Γ ⊢ e ▷ λ m
This syntactic check uses mem E (s) and vars(e), which are sound over-approximations of an instruction and expression memory footprint (the approximation is not complete, e.g. it will include memory accesses done by unreachable code). The RestrCompl rule checks that an instruction verifies some complexity restriction. The rule generates proof obligations in a Hoare logic for cost. These proof obligations are discharged Module path resolution res Γ (p) to module expression

res Γ (p) = res Γ ( m) (if Γ(p) = m : _) res Γ (p.x) = res Γ (m) (if res Γ (p) = struct st 1 ; module x = m : M; st 2 end) res Γ (p(p ′ )) = res Γ (m 0 [x → p ′ ]) (if res Γ (p) = func(x : M) m 0 ) res Γ (p(p ′ )) = (abs K x)(ì p 0 , p ′ ) (if res Γ (p) = (abs K x)(ì p 0 )) Module expression resolution res Γ ( m) res Γ (struct st end) = struct st end res Γ (func(x : M) m) = func(x : M) m res Γ ((abs K x)(ì p)) = (abs K x)(ì p)
Module procedure resolution f-res Γ (m.f ) (note that this includes resolution for function paths f-res

Γ (p.f )) f-res Γ (p.f ) = (proc f ( ì v : ì τ ) → τ r = body) (if Γ(p.f ) = (proc f ( ì v : ì τ ) → τ r = body)) f-res Γ (m.f ) = (proc f ( ì v : ì τ ) → τ r = body) (if res Γ (m) = struct st 1 ; proc f ( ì v : ì τ ) → τ r = body; st 2 end) f-res Γ (m.f ) = (abs K x)(ì p).f (if res Γ (m) = (abs K x)(ì p))
Fig. 9. Resolution functions for paths, module expressions and module procedure.

interactively using the proof system we present later, in Section 4.

RestrCompl

E ⊢ {⊤} s {ψ | t } ⊢ {ψ } r ≤ t r (t + t r • 1 conc ) ≤ compl λ c E ⊢ { _; s; return r } ▷ λ c
Here, the proof obligation E ⊢ {⊤} s {ψ | t } states that the execution of s in any memory has a complexity upper bounded by t, and that the post-condition ψ holds after s's execution. The proof obligation ⊢ {ψ } r ≤ t r upper-bounds the cost of evaluating the return expression r . Finally, the rule checks that the sum of t and t r is compatible with the complexity restriction λ c through the premise (t

+ t r • 1 conc ) ≤ compl λ c .
We leave the precise definition of ≤ compl to Section 4 (see Fig. 13). Intuitively, t is a record of entries of the form (x.f → l f ), each stating that the abstract module x's procedure f has been called at most l c times, plus a special entry (conc → l c ) stating that s execution time, excluding abstract calls, is at most l c . Then,

t 0 ≤ compl λ c checks that t 0 [x.f ] ≤ λ c [x.f ]
for every functor parameter x.f , and that λ c [intr] upper-bounds everything else in t 0 .

Remark 3.1. Note that the complexity checking rule RestrCompl is not extended to typing environment, because the cost Hoare judgment E ⊢ {⊤} s {ψ | t } is not defined for typing environment. While we could probably extend RestrCompl to allow typing in a typing environment Γ, this would complicate a lot the soundness proof of our logic. Indeed, as it stands, we do not need to show closure of Hoare logic derivations under substitution of a module parameter x of type abs param : M by a concrete module m of the same type M (because an environment E cannot contain a declaration of an abstract module of kind param, only of open modules of kind open, which are never substituted, only instantiated). Instead, we only need to show closure under such substitution for typing judgment (not Hoare logic derivations), which simplifies the proof.

Module Resolution

We present the semantics of our module system, which we use to give the semantics of our programming language in Section 5. Our module system semantics is given by a module resolution mechanism, which describes how module expression m are evaluated in a typing environment Γ.

Extended module resolution. Because a module expression m is evaluated in a typing environment Γ that can contain abstract modules (representing open code or functor parameters), the resolved module res Γ (m) may not be a module expression according to the syntactic categories defined in Fig. 21. We let extended module expressions be the elements of the form:

m ::= m | abs K x
Note that it would not make much sense to extend the syntax of module expressions to allow them to contain abstract modules, as abstract modules of kind param are reserved to the type system; and open modules must be introduced at the logical level (in the ambient higher-order logic).

Module resolution. The resolution function res Γ (_) evaluates a module path, in Γ, into a (resolved) extended module expression, which can be a module structure, a functor, or an (potentially applied) abstract module. Mostly, res Γ (_) take care of functor application through the rules:

res Γ (p(p ′ )) = res Γ (m 0 [x → p ′ ]) (if res Γ (p) = func(x : M) m 0 ) res Γ (p(p ′ )) = (abs K x)(ì p 0 , p ′ ) (if res Γ (p) = (abs K x)(ì p 0 ))
(the full definition is in Fig. 9). In the concrete functor case, we must substitute the module identifier x into a path p ′ in a module expression m 0 .

Example 3.1. Consider a typing environment Γ, and the path x.y(z)(v)(w), which must be read as (((x.y)(z))(v))(w). Then, assuming that Γ(z) = abs open z, Γ(v) = m v , Γ(w) = abs param w and:

Γ(x) = struct module y = func(u : _) u end
where m v is some module expression, then res Γ (x.y(z)(v)(w)) = (abs open z)(v, w).

We define the module procedure resolution function f-res Γ (m.f ). A resolved module procedure f-res E (m.f ) is: i) either a concrete procedure declaration (proc f ( ì v : ì τ ) → τ r = body); ii) or the procedure component f of a resolved (potentially applied) abstract module (abs K x)(ì p).f .

COMPLEXITY REASONING IN EASYCRYPT

We now present our Hoare logic for cost, which allows to formally prove complexity upper-bounds of programs. This logic manipulates judgment of the form E ⊢ {ϕ} s {ψ | t }, where s is a statement, ϕ,ψ are assertions, and t is a cost. We leave the assertion language unspecified, and only require that the models of an assertion formula ϕ are memories, and write ν ∈ ϕ whenever ν satisfies ϕ.

Essentially, the judgment E ⊢ {ϕ} s {ψ | t } states that s is a program well-typed in the environment E (e.g. this means that s can only call concrete or abstract procedures declared in E), and that: i) the execution of the program s on any initial memory ν i satisfying the precondition ϕ (i.e. ν i ∈ ϕ) terminates in time at most t; and ii), the final memory ν f obtained by executing s starting from ν i satisfies the post-condition ψ (i.e. ν f ∈ ϕ).

Cost Judgment

A key point of our Hoare logic for cost is that it allows to split the cost of a program s between its concrete and abstract costs, i.e. between the time spent in concrete code, and the time spent in abstract procedures. To reflect this separation between concrete and abstract cost, a cost t is a record of entries mapping each abstract procedure x.f to the number of times this procedure was called, and mapping a special element conc to the concrete execution time (i.e. excluding abstract procedure calls). Since the set of available abstract procedures (and consequently the number of entries in the cost t) depends on the current environment E, we parameterize the notion of cost by the environment E considered: Definition 4.1. A E-cost is an element of the form:

t ::= [conc → k, x 1 .f 1 → k 1 , . . . x l .f l → k l ]
where E is an environment, k, k 1 , . . . , k l are integers, and the x i .f i are all the abstract procedures declared in E. Then [conc → 10; x.f → 0; y.h → 3] represents a concrete cost of 10, at most three calls to y.h, and none to x.f . Definition 4.2. A cost judgment for a statement is an element of the form E ⊢ {ϕ} s {ψ | t } where E must be well-typed, s must be well-typed in E and t must be an E-cost. We define similarly a cost judgment for a procedure E ⊢ {ϕ} F {ψ | t }.

In Fig. 10, we give a graphical representation of a cost judgment for the procedure A(B, C).a, where A and C are concrete modules, and B is an abstract functor with access to C as a parameter. Then, intuitively, the cost judgment:

E ⊢ {⊤} A(B, C).a {⊤ | [conc → t conc , B.b → 1]}
is valid whenever t conc upper-bounds the concrete cost (in hatched gray ) which is the sum of: i) the intrinsic cost of A.a, which is the cost of A.a without counting parameter calls, represented in hatched blue in the figure, and must be at most t a as stated in T A 's restriction; and ii) the sum of the cost of the three calls to C.c.

The cost of the execution of the abstract procedure B.b (in hatched red ), which excludes the two calls B.b makes to C.c, are accounted for by the entry (B.b → 1) in the cost judgment. Note that it is crucial that this excludes the cost of the two calls to C.c, which are already counted in the concrete cost t conc .

Skip

E ⊢ {ϕ } skip {ϕ | 0} Weak E ⊢ {ϕ ′ } s {ψ ′ | t ′ } ϕ ⇒ ϕ ′ ψ ′ ⇒ ψ t ′ ≤ t E ⊢ {ϕ } s {ψ | t } False E ⊢ {⊥} s {ψ | t } Assign ⊢ {ϕ } e ≤ t e E ⊢ {ϕ ∧ ψ [x ← e]} x ← e {ψ | t e } Rand ⊢ {ϕ 0 } d ≤ t ϕ = (ϕ 0 ∧ ∀v ∈ dom(d ).ψ [x ← v]) E ⊢ {ϕ } x $ ← -d {ψ | t } Seq E ⊢ {ϕ } s 1 {ϕ ′ | t 1 } E ⊢ {ϕ ′ } s 2 {ψ | t 2 } E ⊢ {ϕ } s 1 ; s 2 {ψ | t 1 + t 2 } If E ⊢ {ϕ ∧ e } s 1 {ψ | t } E ⊢ {ϕ ∧ ¬e } s 2 {ψ | t } ⊢ {ϕ } e ≤ t e E ⊢ {ϕ } if e then s 1 else s 2 {ψ | t + t e } While I ∧ e ⇒ c ≤ N ∀k, E ⊢ {I ∧ e ∧ c = k } s {I ∧ k < c | t (k )} ∀k ≤ N , ⊢ {I ∧ e ∧ c = k } e ≤ t e (k) ⊢ {I ∧ ¬e } e ≤ t e (N + 1) E ⊢ {I ∧ 0 ≤ c } while e do s {I ∧ ¬e | N i =0 t (i) + N +1 i =0 t e (i)} Call args E (F) = ì v ⊢ {ϕ[ ì v ← ì e ]} ì e ≤ t e E ⊢ {ϕ } F {ψ [x ← ret] | t } E ⊢ {ϕ[ ì v ← ì e ]} x ← call F(ì e ) {ψ | t e + t } Conc f-res E (F) = (proc f ( ì v : ì τ ) → τ r = { _; s; return r }) E ⊢ {ϕ } s {ψ [ret ← r ] | t } ⊢ {ψ } r ≤ t ret E ⊢ {ϕ } F {ψ | t + t ret }
Convention: ret cannot appear in programs (i.e. ret V). Expression cost. We have a second kind of judgment ⊢ {ϕ} e ≤ t e , which states that the cost of evaluating e in any memory satisfying ϕ is at most t e , where t e is an integer, not a E-cost (indeed, an expression cost is always fully concrete, as expressions do not contain procedure calls). We do not provide a complete set of rules for such judgments, as this depends on low-level implementation details and choices, such as data-type representation and libraries implementations. In practice, we give rules for some built-ins, a way for the user to add new rules, and an automatic rewriting mechanism which automatically prove such judgments from the user rules in most cases.

Hoare Logic for Cost Judgment

We present our Hoare logic for cost, which allows to prove cost judgments of programs. Our logic has one rule for each possible program construct (assignment, loop,...), plus some structural rules (e.g. weakening). We start by describing the rules for the basic program constructs (the rules can be found in Fig. 11).

Basically, our cost judgment are standard Hoare logic judgment with the additional cost information, and both aspects must be handled by the rules of our logic.

In some cases, these can be handled separately. E.g. the rule:

If ⊢ {ϕ} e ≤ t e E ⊢ {ϕ ∧ e} s 1 {ψ | t } E ⊢ {ϕ ∧ ¬e} s 2 {ψ | t } E ⊢ {ϕ} if e then s 1 else s 2 {ψ | t + t e }
state that if: i) the evaluation of the condition e takes time at most t e ; ii) the execution of the then branch program s 1 , assuming pre-condition ϕ ∧ e, guarantees the post-condition ψ and takes time at most t; iii) and the execution of the else branch, assuming the pre-condition ϕ ∧ ¬e, guarantees the same post-condition ψ , and also takes time at most t; then the full conditional statement if e then s 1 else s 2 , assuming pre-condition ϕ, guarantees the post-condition ψ in time at most

1:17 Abs f-res E (F) = (abs open x)(ì p).f E(x) = abs open x : (func(ì y : _) sig _ restr θ end) θ [f ] = λ m ∧ λ c λ c = compl[intr : K, z j 1 .f 1 : K 1 , . . . , z j l .f l : K l ] FV(I ) ∩ λ m = ∅ ì k fresh in I ∀i, ∀ ì k ≤ (K 1 , . . . , K l ), ì k[i] < K i → E ⊢ {I ì k} ì p[j i ].f i {I ( ì k + 1 i ) | t i k } E ⊢ {I ì 0} F {∃ ì k, I ì k ∧ ì 0 ≤ ì k ≤ (K 1 , . . . , K l ) | T abs } where T abs = x.f → 1; G → l i=1 K i -1 k =0 (t i k)[G] G x.f Conventions: ì
y can be empty (this corresponds to the non-functor case).

Fig. 12. Abstract call rule for cost judgment.

t + t e . Note that we use the same cost upper-bound t for both branches: essentially, t can be chosen to be the maximum of the execution times of both branches. We designed rules for all basic constructs of the logic. E.g. the assignment rule Assign lets the user provide a dedicated pre-condition ϕ used to upper-bound the cost of evaluating e4 ; and the weakening rule Weak is the standard Hoare logic weakening rule, with an additional premise t ′ ≤ t.

Other rules are more involved, and require the user to show simultaneously invariants of the memory state of the program and cost upper-bounds. This is the case of the abstract call rule, and of the instantiation rule.

Abstract Call Rule

The abstract call rule allows to upper-bound the cost of a call to an abstract procedure F. To ease the presentation, we first present a version of the rule for usual Hoare judgment without costs, and explain how to add costs after.

abs-partial f-res E (F) = (abs open x)(ì p).f E(x) = abs open x : (func(ì y : _) sig _ restr θ end) θ [f ] = λ m ∧ _ FV(I ) ∩ λ m = ∅ ∀p 0 ∈ ì p, ∀д ∈ procs E (p 0 ), E ⊢ {I } p 0 .д {I } E ⊢ {I } F {I }
First, the function path F is resolved to (abs open x)(ì p).f , i.e. a call to the procedure f of an abstract functor x applied to the modules ì p (the case where x is not a functor is handled by taking ì p = ϵ). Then, x's module type is lookup in E, and we retrieve the module restriction θ attached to it. The rule allows to prove that some formula I is an invariant of the abstract call, by showing two things.

First, we show that I is an invariant of x.f , excluding calls to the functor parameters. This is done by checking that x.f cannot access the variables used in I , using its memory restriction λ m (looked-up by the premise θ

[f ] = λ m ∧ _) and requiring that FV(I ) ∩ λ m = ∅ .
Then, we prove that I is an invariant of x.f 's calls to functor parameters. This is guaranteed by requiring that for every functor parameter p 0 ∈ ì p, for any of p 0 's procedure д ∈ procs E (p 0 ), the judgment E ⊢ {I } p 0 .д {I } is valid.

Abstract Call Rule. We now present our Abs rule for cost judgments, which is given in Fig. 12. Essentially, the cost of the call to x(ì p).f is decomposed between:

• the intrinsic cost of x.f excluding the cost of the calls to x's functor parameters. This is accounted for by the entry (x.f → 1) in the final cost T abs . • the cost of the calls to x.f functor parameters, which are enumerated in the restriction:

λ c = compl[intr : K, z j 1 .f 1 : K 1 , . . . , z j l .f l : K l ] Instantiation M l = func(ì y : ì M) sig S l restr θ end E ⊢ x m : erase compl (M l ) ì z fresh in E ∀f ∈ procs(S l ), (E, module ì z : abs open ì M ⊢ {⊤} m(ì z).f {⊤ | t f }) ∀f ∈ procs(S l ), t f ≤ compl θ [f ] E, module x = abs open : M l ⊢ {ϕ} s {ψ | t s } E, module x = m : M l ⊢ {ϕ} s {ψ | T ins }
where:

T ins = G → t s [G] + f ∈procs(S l ) t s [x.f ] • t f [G] t f ≤ compl θ [f ] = ∀z 0 ∈ ì z, ∀д ∈ procs( ì M[z o ]), t f [z 0 .д] ≤ θ [f ][z 0 .д] ∧ t f [conc] + A∈abs(E) h ∈procs E (A) t f [A.h] • intr E (A.h) ≤ θ [f ][intr]
Conventions: intr E (A.h) is the intr field in the complexity restriction of the abstract module procedure A.h in E. We require, for every i, a bound on the cost of the k-th call to the functor argument z j i procedure's f i , where k can range anywhere between 0 and the maximum number of calls x.f can make to z j i , which is K i . The cost of the k-th call to z j i .f i is bounded by

(t i k)
where

k = ì k[i] and: E ⊢ {I ì k} ì p[j i ].f i {I ( ì k + 1 i ) | t i k}
To improve precision, we let the invariant I depend on the number of calls to the functor parameters through the integer vector ì k. After calling ì p[j i ].f i , we update ì k by adding one to its i-th entry (1 i is the vector where the i-th entry is one and all other entries are zero). The final cost T abs (except for x.f ) is obtained by taking the sum, over all functor parameters and number of calls to this functor parameter, of the cost of each call.

Instantiation Rule

The Instantiation rule, given in Fig. 13, allows to instantiate an abstract module x by a concrete module m. Assume that we can upper-bound the cost of a statement s by t s , when x is abstract:

E, module x = abs open : M l ⊢ {ϕ} s {ψ | t s }
Then we can instantiate x by a concrete module m as long as m complies with the module signature M l , which is checked through two conditions.

First, we check that m has the correct module type, except for complexity restrictions, through the premise E ⊢ x m : erase compl (M l )

Then, we check that m satisfies the complexity restriction θ in M l , by requiring that for any procedure f of x:

E, module ì z : abs open ì M ⊢ {⊤} m(ì z).f {⊤ | t f } where t f must respect θ [f ], which is guaranteed by t f ≤ compl θ [f ],
which does two checks:

• first, it ensures that the number of calls to any functor parameter z 0 of x done by m.f is upper-bounded by θ [f ][z 0 ]. • then, it verifies that the bound of x's intrinsic cost θ [f ][intr] upper-bounds the cost of the execution of m.f , excluding functor parameter calls, through the condition:

t f [conc] + A∈abs(E) h ∈procs E (A) t f [A.h] • intr E (A.h) ≤ θ [f ][intr]
ACM Trans. Priv. Sec., Vol. The final cost T ins (in Fig. 13) is the sum of the cost t s of s (which excludes the cost of x's procedures), plus the sum, for any procedure f of x, of the number of times s called x.f (which is t s [x.f ]), times the cost of x.f (which is t f ).

INSTRUMENTED SEMANTICS

We now define the denotational semantics of our programming language and cost judgments. We first quickly introduce the main aspects of our semantics below, before defining it formally in the rest of the section. We use this semantics to state our main soundness theorem. The proof of our main theorem is postponed to Appendix D.

Program semantics. The semantics s E, ρ ν of our language depends on the initial memory ν , the environment E, and on the interpretation ρ of E's abstract modules. Essentially, s E, ρ ν is a discrete distribution over M × N, where the integer component is the cost of evaluating s in (E, ρ), starting from the memory ν. Then, the E-cost of an instruction s under memory ν and interpretation of E's abstract modules ρ, denoted by cost E, ρ ν (s) ∈ N ∪ {+∞}, is the maximum execution cost in any final memory, defined as:

cost E, ρ ν (s) = inf c ′ | Pr (_, c) ← s E, ρ ν ; c ≤ c ′ = 1 (1)
Judgments semantics. Basically, the judgment E ⊢ {ϕ} s {ψ | t } states that: i) the memory ν obtained after executing s in an initial memory ν ∈ ϕ must satisfy ψ ; ii) the complexity of the instruction s is upper-bounded by the complexity of the concrete code in s, plus the sum over all abstract oracles A.f of the number of calls to A.f times the intrinsic complexity of A.f . Formally:

cost E, ρ ν (s) ≤ t[conc] + A∈abs(E) f ∈procs(E(A)) t[A.f ] • compl E, ρ A.f
where compl E, ρ A.f is the intrinsic complexity of the procedure A.f , i.e. its complexity excluding calls to A's functor parameters.

Semantics

We now present the semantics of our programs. For any set A, we denote by D(A) the set of discrete sub-distributions over A -i.e. the set of function µ :

A → [0, 1] with discrete support s.t. µ is summable and |µ | = x µ(x) ≤ 1. For x ∈ A, the Dirac distribution at x is written 1 A x or 1 x when A is clear from the context. If µ ∈ D(A) and µ ′ ∈ A → D(B), the expected distribution of µ ′ ∈ D(B) when ranging over µ, written E x ∼µ [µ ′ (x)] or E µ [µ ′ ], is defined as E µ [µ ′ ] = b ∈ B → a ∈A µ(a) µ ′ (a)(b). For µ ′ ∈ D(A) and f : A → B, the marginal of µ ′ w.r.t. f , written f # (µ ′ ) ∈ D(B), is defined as f # (µ ′ ) = b → a ∈A |f (a)=b µ ′ (a). We write π # 1 (resp. π # 2 )
for resp. the first and second marginal -i.e. when f is resp. the first and second projection. For any base type τ ∈ B, we assume an interpretation domain V τ . We let V be the set of all possible values ∪ τ ∈B V τ . A memory ν ∈ M is a function from V to V . We write ν [x] for ν (x). For ν ∈ M and v ∈ V , we write ν[x ← v] for the memory that maps x to v and y to ν [y] for y x.

Expressions semantics. For any operator

f ∈ F E with type τ 1 × • • • × τ n → τ , we assume given its semantics f : V τ 1 × • • • × V τ n → V τ , and the cost of its evaluation c E (f , •) : V τ 1 × • • • × V τ n → N. skip E, ρ ν = 1 (ν,0) abort E, ρ ν = 0 s 1 ; s 2 E, ρ ν = E (ν ′ ,c ′ )∼ s 1 E, ρ ν [ s 2 E, ρ ν ′ ⊕ c ′ ] x ← e E, ρ ν = 1 (ν [x ← e ν ],c E (e,ν )) x $ ← -d E, ρ ν = E v∼ d ν [1 (ν [x ←v],c D (d,ν )) ] if e then s 1 else s 2 E, ρ ν =        s 1 E, ρ ν ⊕ c E (e, ν ) if e ν 0 s 2 E, ρ ν ⊕ c E (e, ν ) otherwise while e do s E, ρ ν = lim n →∞ loop e,s n E, ρ ν
where loop e,s n+1 = if e then (s; loop e,s n ) else skip and loop e,s 0 = if e then abort else skip The semantics e ν : M → V of a well-typed expression e in a memory ν is defined inductively by:

Moreover, if f-res E (m.f ) = proc f ( ì v : ì τ ) → τ r = { _; s; return r }: x ← call m.f (ì e ) E, ρ ν = let ν 0 = ν [ ì v ← ì e ν ] in E (ν ′ ,c ′ )∼ s E, ρ ν 0 [1 ν ′ [x ← r ν ′ ],c ′ +c E (ì e,ν )+c E (r,ν ′ ) ] And if f-res E (m.f ) = (abs open x)(ì p).f : x ← call m.f (ì e ) E, ρ ν = x ← call ρ(x)(ì p).f (ì e ) E, ρ ν
e ν = ν (x) if e = x ∈ V f ( e 1 ν , . . . , e n ν ) if e = f (e 1 , . . . , e 1 )
And the cost of the evaluation of a well-typed expression c E (e, •) : M → N is defined by:

c E (e, ν ) =          1 if e = x ∈ V c f + 1≤i ≤n c E (e i , ν ) if e = f (e 1 , . . . , e n ) and c f = c E (f , e 1 ν , . . . , e n ν )
For technical reasons, we assume that there exists one operator with a non-zero cost. 5For any distribution operator d ∈ F D with type τ 1 × • • • × τ n → τ , we assume given its semantics

d : V τ 1 × • • • × V τ n → D(V τ ), and the cost of its evaluation c D (d, •) : V τ 1 × • • • × V τ n → N. We define similarly d ν : M → D(V ) and c D (d, •) : M → N.
Environment and E-pre-interpretation. To give the semantics of a program in an environment E, we need an interpretation of E's abstract modules. A E-pre-interpretation is a function ρ from E's abstract modules to module expressions, with the correct types, except for complexity restrictions.

We will specify what it means for a module expression to verify a complexity restriction later, after having defined the semantics of our language. Definition 5.1. Let erase compl (M) be the module signature M where every complexity restriction λ c has been erased, by replacing it by ⊤. Then ρ is a E-pre-interpretation if and only if for every x such that E = E 1 ; module x = abs open : M l ; E 2 , we have E 1 ⊢ ϵ ρ(x) : erase compl (M l ).

Note that we type ρ(x) in E 1 , which lets the interpretation of x use any module or abstract module declared before x in E.

Programs semantics. If µ ∈ D(M × N) and n ∈ N, we write µ ⊕ n for the distribution f # (µ) where f : (m, c) → (m, c + n). Let E be a well-typed environment, and s be a well-typed instruction in E, i.e. such that E ⊢ s. The E-denotational semantics of an instruction s under the memory ν and E-pre-interpretation ρ, written s E, ρ ν ∈ D(M × N), is defined in Fig. 14. We give the semantics for an extended syntax, which allows procedure calls to be of the form x ← call m.f (ì e ) where m is a module expression. Note that this subsumes the syntax of statements, since a module expression m can be a module path p. This allows to concisely define the semantics of a call to an abstract procedure (abs open x)(ì p).f as the semantics of a call to ρ(x)(ì p).f . The E-cost of an instruction s under memory ν and E-pre-interpretation ρ, denoted by cost

E, ρ ν (s) ∈ N ∪ {+∞}, is defined as: cost E, ρ ν (s) = sup(supp(π # 2 ( s E, ρ ν )))
where supp is the support of a distribution (this definition is equivalent to the one given in Equ. 1).

Cost Judgement Semantics and Soundness of our Proof System

To define the semantics of our cost judgments, we need two additional complexity measures: the number of calls a program execution makes to some abstract procedure, and the intrinsic cost of a program execution (i.e. the cost of the program without the cost of parameters calls). For space reasons, these additional complexity measures are defined in Appendix B.

Soundness. We now have all the tools to define the semantics of our expression and program cost judgments.

supp(π # 1 ( s E, ρ ν )) ⊆ ψ ∧ cost E, ρ ν (s) ≤ t[conc] + A∈abs(E)f ∈procs(E(A)) t[A.f ] • compl E, ρ A.f
where a E-interpretation is a E-pre-interpretation mapping abstract modules to concrete module satisfying the required memory and complexity restrictions, and compl E, ρ A.f is the intrinsic complexity of the procedure A.f , i.e. its complexity excluding calls to A's functor parameters (the detailed definition is postponed to Appendix B).

Basically, the complexity of the instruction s is upper-bounded by the complexity of the concrete code in s, plus the sum over all abstract oracles A.f of the number of calls to A.f times the intrinsic complexity of A.f .

We are now ready to state our main theorem showing the soundness of our Hoare logic for cost.

EXAMPLE: UNIVERSAL COMPOSABILITY

UC security guarantees that a protocol π 1 can safely replace a protocol π 2 while preserving both the functionality and the security of the overall system. The most common application of this framework is to set π 2 to be an idealized protocol that assumes a trusted-third-party (TTP) to which parties delegate the computation; the specification of the TTP is called an ideal functionality F . An ideal functionality F defines what protocol π 1 should achieve both in terms of correctness and security to securely replace the TTP. Moreover, F can be used as an ideal sub-component when designing higher-level protocols, which then can be instantiated with protocol π 1 to obtain a fully concrete real-world protocol.

The UC framework defines an execution model where protocol participants, attackers and contexts are modeled as Interactive Turing Machines (ITM). The model was carefully designed to give a good balance between expressive power-e.g., one can capture complex interactions in distributed protocols involving multiple parties in a variety of communication models, various forms of corruption, etc.-and a tailored (and relatively simple) resource analysis mechanism that permits keeping track of the computing resources available to both honest and malicious parties.

The model is described in detail in [START_REF] Canetti | Universally Composable Security: A New Paradigm for Cryptographic Protocols[END_REF][START_REF] Canetti | Universally Composable Security: A New Paradigm for Cryptographic Protocols[END_REF]. However, most UC proofs found in the literature refer only to a common understanding of the semantics of the execution model and a set of high-level restrictions that are inherent to the model. These include the allowed interactions between different machines, the order in which machines are activated, predefined sequences of events, etc. More fine-grained descriptions of the execution model are sometimes introduced locally in proofs, when they are needed to deal with more subtle points or technicalities that can only be clarified at the cost of extra details. This stands in contrast with typical game-based proofs for simpler cryptographic primitives [START_REF] Barthe | Formal certification of code-based cryptographic proofs[END_REF], where security proofs are given in great detail. This is one of the reasons why, while there has been impressive progress in machine-checking game-based proofs [START_REF] Barbosa | SoK: Computer-Aided Cryptography[END_REF], we are only now giving the first steps in formalizing proofs in the UC setting [START_REF] Canetti | EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security[END_REF][START_REF] Haagh | Computer-Aided Proofs for Multiparty Computation with Active Security[END_REF][START_REF] Liao | ILC: a calculus for composable, computational cryptography[END_REF]. Another reason is that the ITM model for communication is difficult to express in procedure-based semantics offered by tools that target game-based proofs.

To overcome these difficulties, we propose a new approach to machine-checking UC proofs that shares many features of the simplified version of UC proposed by Canetti, Cohen and Lindell in [START_REF] Canetti | A Simpler Variant of Universally Composable Security for Standard Multiparty Computation[END_REF]. As in [START_REF] Canetti | A Simpler Variant of Universally Composable Security for Standard Multiparty Computation[END_REF], we statically fix the machines/modules in the execution model and we allow an adversarial entity to control which module gets to be executed next, rather than allowing machines to pass control between them more freely as in the original UC execution model. The crucial difference to the ITM execution model is that the above interactions are procedure-based, which means that whenever the environment passes control to the protocol, the internal protocol structure will follow a procedure call tree that guarantees (excluding the possibility of non-terminating code) that control returns to the environment. 6 As in [START_REF] Canetti | A Simpler Variant of Universally Composable Security for Standard Multiparty Computation[END_REF], we lose some expressiveness, but we do not go as far as hard-wiring a specific communications model for protocols based on authenticated channels; instead, we leave it to the protocol designer to specify the communications model by using an appropriate module structure. We recover the authenticated communications model of [START_REF] Canetti | A Simpler Variant of Universally Composable Security for Standard Multiparty Computation[END_REF] by explicitly defining a hybrid real-world, in which concrete modules for ideal authenticated channels are available to the communicating parties. We discuss the trade-offs associated with our approach more in depth at the end of this section, drawing a parallel to the work in [START_REF] Canetti | EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security[END_REF].

Mechanized Formalization in EasyCrypt

We propose a natural simplification of the UC execution model that is based on EasyCrypt modules and show that this opens the way for a lightweight formalization of UC proofs. This formalization has been conducted in our extension of EasyCrypt (the proofs of the lemmas and theorems of this section are fully mechanized).

Protocols and Functionalities as EasyCrypt modules. The basic component in our UC execution model is a module of type PROTOCOL given in Fig. 15. Inhabitants of this type represent a full real-world configuration-a distributed protocol executed by a fixed number of parties-or an ideal-world configuration-an ideal functionality executing a protocol as a trusted-third party. The type of a protocol has a fixed interface, but it is parametric on the types of values exchanged via this interface. The fixed interface is divided into three parts: i) init allows modeling some global protocol setup; ii) IO captures the interaction of a higher level protocol using this protocol as a sub-component; and iii) BACKDOORS captures the interaction of an adversary with the protocol during its execution.

When we define real-world protocols, a module of type PROTOCOL will be constructed from sub-modules that emulate the various parties and the communications channels between them. In this case, BACKDOORS models adversarial power in this communication model. For ideal-world protocols, a PROTOCOL is typically a flat description of the ideal computation in a single module; here BACKDOORS models unavoidable leakage (e.g., the length of secret inputs or the states of parties in an interactive protocol) and external influence over the operation of the trusted-third party (e.g., blocking the computation to model a possible denial of service attack). 7Execution Model. The real-and ideal-world configurations are composed by a statically determined set of modules, which communicate with each-other using a set of hardwired interfaces. The execution model is defined by an experiment in which an external environment interacts with the protocol via its IO and BACKDOORS interfaces until, eventually, it outputs a boolean value (Fig. 16). The IO interface allows the environment to pass an input to the protocol using inputs or to retrieve an output produced by the protocol using outputs. For example in the real-world, the environment can use these procedures to give input to or obtain an output from one of the sub-modules that represent the computing parties involved in the protocol. The BACKDOORS interface allows the environment to read some message that may be produced by the protocol using backdoor or make one of the protocol sub-components (parties) advance in its execution using step to deliver a message. We describe now the typical sequence of events in a real-world execution; the ideal-world will become clear when we describe the notion of UC emulation below. When the adversarial environment uses the IO interface to pass input to a computing party, this may trigger the computing party to perform some computations and, in turn, provide inputs to other sub-modules included in the protocol description; in most cases this will correspond to sending a message using an idealized communications channel represented by an ideal functionality. 8 Our convention is that inputs calls do not allow obtaining information back (the return type is unit). This means that any outputs produced by parties need to be pulled by the environment with separate calls to outputs. Similarly, when the environment asks a party for an output, the party may perform some computation and call the outputs interface of a hybrid ideal functionality (e.g., to see if a message has been delivered) before returning the output to the environment.

The BACKDOORS interface follows these conventions closely. The backdoor method allows the environment to retrieve leakage that may be available for it to collect (e.g., the public part of a party's state, or a buffered message in an authenticated channel). The step procedure allows the environment to pass control to any module inside the protocol; this is important to make sure that the environment always has full control of the liveness of the execution model and can schedule the execution of the various processes at will whenever there are several possible lines of execution.

UC emulation. The central notion to Universal Composability is called UC-emulation, which is a relation between two protocols π 1 and π 2 : if π 1 UC-emulates π 2 with small advantage ϵ then π 1 can replace π 2 in any context (within a complexity class). Definition 6.1 (UC emulation). Protocol π 1 UC emulates π 2 under complexity restrictions c sim and c env and advantage bound ϵ if

∃S ∈ τ π 1 , π 2 ,c sim sim , ∀Z ∈ τ π 1 , π 2 , S,c env env , | Pr[ Z(π 1 ) : ⊤ ] -Pr[ Z(⟨π 2 ∥ S(π 2 )⟩) : ⊤ ] | ≤ ϵ
We write this as Adv uc c sim ,c env (π 1 , π 2 ) ≤ ϵ.

The first probability term corresponds to the event that the environment returns true in the real-world execution model described above, i.e., in game UC_emul parameterized with ENV = Z and P = π 1 . The second probability term corresponds to the equivalent event in the ideal-world (or reference) execution model where, as shown in Fig. 17 (right), π 2 is typically an ideal functionality; this corresponds to game UC_emul parameterized with ENV = Z and a protocol P that results from attaching S to the BACKDOORS interface of π 2 . We denote this ideal-world P by ⟨π 2 ∥ S(π 2 )⟩, corresponding to the EasyCrypt functor CompS also shown in Fig. 16.

UC-emulation imposes that a simulator S is capable to fool any environment by presenting a view that is fully consistent with the real-world, while learning only what the BACKDOORS interface of π 2 allows. If such a simulator exists, then clearly π 2 cannot be worse than π 1 in the information it reveals to the environment via its BACKDOORS interface. 9 Our UC-emulation definition quantifies over simulators and environments using types that give a full characterization of their use of resources, including the ability to access memory, number and types of procedure calls and intrinsic computational costs. The memory access restrictions are depicted in Fig. 17, and they can be easily matched to the standard restrictions in the UC framework. Not shown are the cost restrictions, which give explicit bounds for the resources used by various parts of the execution model; these are crucial for obtaining, not only a meaningful definition, but also for obtaining meaningful reductions to computational assumptions, as will be seen below.

Let us examine the types of Z and S in more detail. We first note that the definition of emulation is parametric in the resource restrictions c sim and c env . Clearly the IO interface of π 2 must match the type of the IO interface of π 1 , which is consistent with the goal that π 1 can replace π 2 in any context, and this is enforced by our type system. This need not be the case for the BACKDOORS interface and, in fact, if π 2 is an ideal functionality, the BACKDOORS interface in the ideal world is of a different nature altogether than the one in the real world: it specifies leakage and adversarial control that are unavoidable even when the functionality is executed by a trusted third-party on behalf of the parties. The type of the simulator S is given by τ π 1 , π 2 ,c sim sim , which defines the type of modules that has access to the BACKDOORS interface of π 2 , exposes the BACKDOORS interface of π 1 and is restricted memory-wise to exclude the memory of π 2 and resource-wise by c sim . Note that, if S could look inside the ideal functionality, then it would know all the information that is also given to the real-world protocol: a trivial simulator would always exist and the definition would be meaningless because all protocols would be secure. The type of the environment is given by τ π 1 , π 2 , S,c env env , the type of modules that have oracle access to the IO and BACKDOORS interfaces of π 1 , and are restricted memory-wise to exclude the memories of π 1 , π 2 and S, and resource-wise by c env . In this case, if the environment could look inside π 1 , π 2 or S it could directly detect with which world it is interacting, and no protocol would be secure. For concreteness, the cost restriction on the type of the environment imposed by c env is of the form:

c env := compl[intr : c 1 , π .inputs : c 2 , π .outputs : c 3 , π .backdoor : c 4 , π .step : c 5 ]
where type refinements can set c i to depend on the types of other modules in the context.

Warm-up: Transitivity of UC emulation

It is easy to show that UC-emulation is a transitive relation: if π 1 UC-emulates π 2 and this, in turn, UC-emulates π 3 , then π 1 UC-emulates π 3 . When stating this lemma in EasyCrypt we move the existential quantifications over the simulators in the hypotheses to global universal quantifications; this logically equivalent formulation allows us to refer to the memory of these simulators when quantifying over all adversarial environments in the consequence: we quantify only over those that cannot look inside the simulators that are assumed to exist by hypothesis, which is a natural (and necessary) restriction. In other examples we use the same approach. The lemma is stated in EasyCrypt as follows (we adapt the Adv uc, S

•, • (•, •) notation by indicating the universally quantified simulator S in superscript). Lemma 6.1 (Transitivity). For all ϵ 1,2 , ϵ 2,3 ∈ R + , all protocols π 1 , π 2 and π 3 s.t. the IO interfaces of all three protocols are of the same type, all cost restrictions c sim(1,2) , c sim(2,3) and all simulators S 1,2 ∈ τ

π 1 , π 2 ,c sim(1, 2) sim , S 2,3 ∈ τ π 2 , π 3 ,c sim(2, 3) sim
, we have that:

Adv uc, S 1, 2 c sim(1, 2) , ĉenv(1,2) (π 1 , π 2 ) ≤ ϵ 1,2 ⇒ Adv uc, S 2, 3 c sim(2, 3) , ĉenv(2,3) (π 2 , π 3 ) ≤ ϵ 2,3 ⇒ Adv uc ĉsim(1,3) ,c env(1, 3) (π 1 , π 3 ) ≤ ϵ 1,2 + ϵ 2,3
where ĉsim(1,3) corresponds to the cost of sequentially composing S 1,2 and S 2,3 , ĉenv(2,3) must allow for an adversarial environment that results from converting a distinguisher between π 1 and π 3 in c env [START_REF] Albert | Termination and Cost Analysis with COSTA and its User Interfaces[END_REF][START_REF] Bacelar Almeida | Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3[END_REF] and composing it with S 1,2 , and ĉenv(1,2) = c env [START_REF] Albert | Termination and Cost Analysis with COSTA and its User Interfaces[END_REF][START_REF] Bacelar Almeida | Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3[END_REF] .

In the statement of the lemma we use notation ĉ to denote the fact that these cost restrictions are fixed as a function of the costs of other algorithms: intuitively, the cost of the environment in the consequence is free and it constrains the costs of environments in the hypotheses; then, if for some cost restrictions c sim(1,2) and c sim(2,3) the hypotheses hold, these in turn fix the cost of the simulator we give as a witness. This pattern is observable in the remaining examples we give in this section.

From the proof, we get a witness simulator S 1,3 = SeqS(S 2,3 , S 1,2 ) that results from plugging together the two simulators implied by the assumptions: intuitively, S 2,3 is able to interact with π 3 and emulate the BACKDOORS of π 2 , and this is sufficient to enable S 1,2 to emulate the BACKDOORS interface of π 1 , as required. Technically, the proof shows first that one can break down S 1,3 and put π 2 in the place of CompS(π 3 , S 2,3 ). To show this, we aggregate S 1,2 into the environment to construct a new environment that would break π 2 if such a modification was noticeable, contradicting the second hypothesis. The proof then follows by applying the first hypothesis. Note that this proof strategy is visible in the resources used by S 1,3 , since they are those required to run the composed module SeqS(S 2,3 , S 1,2 ). Moreover, the quantification over the resources of the environments in the second hypothesis must accommodate an environment that absorbs simulator S 1,2 and runs it internally.

The dummy adversary in UC

The standard notion of UC emulation [START_REF] Canetti | Universally Composable Security: A New Paradigm for Cryptographic Protocols[END_REF][START_REF] Canetti | Universally Composable Security: A New Paradigm for Cryptographic Protocols[END_REF] enriches the real-world with an explicit adversary A representing an attacker that has access to the real-world BACKDOORS interface and colludes with the environment to break the protocol. In this case, the real-and ideal-world execution models Consider the functor in Fig. 18, which extends any real-world protocol with abstract adversary A (A in EasyCrypt notation) at its BACKDOORS interface. The type of A is parametric in the BACK-DOORS offered by the protocol in our basic execution model, and it fixes the type of the BACK-DOORS interface in the extended execution model NONDUMMY.PROTOCOL. This means that when we quantify over such adversaries, we quantify also over the potential forms of environment-toadversary information exchange. The following theorem shows that we do not lose generality by working with an (implicit) dummy adversary in our execution model. Theorem 6.2 (Dummy Adversary). UC emulation is equivalent to UC emulation with an explicit real-world adversary. More precisely:

• Emulation with an implicit dummy adversary implies emulation with an explicit arbitrary adversary: For all ϵ ∈ R + , all protocols π 1 and π 2 with IO interfaces of the same type, all complexity restrictions c sim , c env and all simulators S ∈ τ π 1 , π 2 ,c sim sim , we have

Adv uc, S c sim ,c env (π 1 , π 2 ) ≤ ϵ ⇒ ∀A ∈ τ adv , Adv uc ĉsim ,c env (⟨π 1 ∥ A(π 1 )⟩, π 2 )
≤ ϵ where ĉsim allows for a simulator S ′ that combines adversary A and simulator S.

• Emulation with an implicit dummy adversary is implied by emulation with an explicit arbitrary adversary: For all ϵ ∈ R + , all protocols π 1 and π 2 with IO interfaces of the same type, all complexity restrictions c sim , c env and all simulator memory spaces M, we have

∀A ∈ τ adv , Adv uc, M c sim ,c env (⟨π 1 ∥ A(π 1 )⟩, π 2 ) ≤ ϵ ⇒ Adv uc, M c sim ,c env (π 1 , π 2 )
≤ ϵ where τ adv accommodates the dummy adversary.

Our proof gives a simulator S ′ for the first part of the theorem that joins together simulator S and adversary A: intuitively the new simulator uses the existing one to fool the (non-dummy) real-world adversary into thinking it is interacting with the real-world protocol and, in this way, it can offer the expected BACKDOORS view generated by A to the environment. The resources used by S ′ are those required to run the composition of S and A. The proof of the second part of the theorem is more interesting: we construct an explicit dummy adversary and use this to instantiate the hypothesis and obtain a simulator for this adversary, which we then show must also work when the dummy adversary is only implicit: this second step is an equivalence proof showing that, if the simulator matches the explicit dummy adversary which just passes information along, then it is also good when the environment is calling the protocols' BACKDOORS interface directly. The resulting simulator is therefore guaranteed to belong to the same cost-annotated type over which we quantify existentially in the hypothesis.

We note a technicality in the second part of the theorem: since the hypothesis quantifies over adversaries before quantifying existentially over simulators, we cannot use the approach adopted in the transitivity proof and in the first part of the theorem, where we use global universal quantifications over hypothesized simulators. Instead, we quantify globally over a memory space M, restrict simulators in the hypothesis to only use M, and prevent other algorithms to interfere with this memory space where appropriate (we abuse notation by indicating M in Adv uc to denote this).

Universal Composability

The fundamental theorem of Universal Composability is stated in our EasyCrypt formalization as follows.

Theorem 6.3 (Universal Composability). For all ϵ ρ , ϵ π ∈ R + , all ideal functionalities f , F , all protocols ρ(f ) and π , such that the IO interfaces of π and f (resp. ρ and F ) are of the same type, all cost restrictions c sim(ρ) , c sim(π ) , and all simulators S ρ ∈ τ

ρ(f ), F,c sim(ρ ) sim and S π ∈ τ π,f ,c sim(π ) sim
, we have:

Adv uc, S π c sim(π ) , ĉenv(π ) (π , f ) ≤ ϵ π ⇒ Adv uc, S ρ c sim(ρ ) , ĉenv(ρ) (ρ(f ), F ) ≤ ϵ ρ ⇒ Adv uc ĉsim ,c env (ρ(π ), F ) ≤ ϵ ρ + ϵ π
where ĉenv(π ) accommodates an environment that internally uses c env resources and additionally runs ρ, ĉsim corresponds to the cost of composing S π and S ρ , ĉenv(ρ) allows for an adversarial environment built by composing S π with an environment in c env .

This theorem establishes that any protocol ρ(f ) that UC-emulates a functionality F when relying on an ideal sub-component f offers the same level of security when it is instantiated with a protocol π that UC-emulates f . The proof first shows that the simulator S π that exists by hypothesis can be converted into a simulator that justifies that ρ(π ) UC-emulates ρ(f ): intuitively this new simulator uses S π when interacting with the backdoors of f and just passes along the environment's interactions with the backdoors of ρ. This part of the proof combines any successful environment Z against the composed protocol into a successful environment that absorbs ρ and breaks π . This justifies the cost restriction on c env . Then, we know by hypothesis that ρ(f ) UC emulates F , and the result follows by applying the transitivity lemma, which also explains the remaining cost restrictions.

Example: Composing key exchange with encryption. We conclude this section with an example of the use of our framework and general lemmas stated above for concrete protocols. Consider the code snippets in Fig. 19. On the left we show the inner structure of a two-party protocol formalization (Diffie-Hellman) when one assumes an ideal sub-component (in this case a bi-directional ideal authenticated channel F2Auth exposing IO interface Pi.REAL.IO). The full real-world configuration is obtained by applying a functor CompRF that composes this protocol with F2Auth and exposes the backdoors of both DHKE and F2Auth in a combined BACKDOORS interface. The IO interface to this real-world protocol is simply the input/output interface for both parties; parties take as input a role (initiator/responder) and the identities of parties involved in the protocol (type unit pkg); they output a session key when the protocol completes.

The Initiator code is shown in Fig. 20. On initialization it samples its ephemeral key pair and resets the derived key. When the environment provides input, which includes the identities of the parties that will take part in the key exchange, the ephemeral public key is transmitted via one of the ideal authenticated channels. The party then returns control to the environment (note that delivering a message to the authenticated channel does not pass control to the authenticated channel). When the environment calls step, the initiator checks the incoming ideal channel to see if it received a message. At any point the environment can check the initiator output using output. The backdoor interface provides no information, since all communications go through the authenticated channels. The responder code is symmetric.

The example starts with a proof that the Diffie-Hellman protocol on the left of Fig. 19 UCemulates the ideal functionality for key exchange shown on the right of Fig. 19 in a hybrid-real world where the parties have access to authenticated channels. The FKE functionality runs internally a state machine that waits for both parties to provide input, and allows an adversary/simulator interacting with its BACKDOORS interface to control when the different parties obtain a fresh shared secret key. This result is stated as follows; note the accounting of resources spent by the combined Diffie-Hellman attacker, making it explicit that the DDH assumption must be valid for such an attacker. Lemma 6.4 (Security of DHKE). Fix c ddh ∈ R + and let ϵ DDH be the maximum advantage of any DDH attacker against the group over which we implement DHKE. Then, we have that

Adv uc

c sim(DHKE) ,c env(DHKE) (DHKE(F2Auth), FKE) ≤ ϵ DDH where c sim(DHKE) is the cost of a concrete simulator S DHKE that just samples random group elements as the protocol messages and mimics the states of the real-world parties and F2Auth; c env(DHKE) must be such that c ddh accommodates the cost of an adversary that runs internally the entire UC emulation experiment (including the environment) and interpolates between the real and ideal worlds, depending on the external DDH challenge.

The second result shows that the ideal functionality for key exchange can be combined with one-time-pad encryption to transform a one-shot authenticated channel into a one-shot secure channel that also guarantees confidentiality. Formally: Lemma 6.5 (Security of OTP). Fix any c env(OTP) . Then we have Adv uc c sim(OTP) ,c env(OTP) (OTP(FKE, FAuth), FSC) = 0 where c sim(OTP) is the cost of a concrete simulator S OTP that just samples a random string in place of the ciphertext and mimics the states of the real-world parties, FKE and FAuth.

Here, FSC represents the secure channel ideal functionality, which operates exactly as Fauth, but does not leak the transmitted message; leakage includes only information on the state of the channel. The protocol runs in a hybrid world where it has access to both FKE and Fauth, uses the former to obtain a shared key between the two parties, and then transmits the one-time-padded message using Fauth. We apply our Universal Composability theorem to derive that FKE can be replaced by the DHKE protocol, resulting in a protocol that still UC-emulates the secure channel functionality. The final theorem is stated as follows. Theorem 6.6 (Security of OTP composed with DHKE). Fix c ddh ∈ R + and let ϵ DDH be the maximum advantage of any DDH attacker against the group over which we implement DHKE. Then Adv uc c sim ,c env (OTP(DHKE, FAuth), FSC) ≤ ϵ DDH where c env is constrained so that c env(DHKE) accommodates an environment that internally uses c env resources and additionally runs OTP, and c sim corresponds to the cost of composing S OTP and S DHKE .

The crucial application of the complexity restrictions is visible in the attacker against the DDH assumption, which now has a more complex structure that results from the application of the composition theorem: for this application of composition to be meaningful, it is crucial that the global environment is computationally bounded (even though the OTP protocol is informationtheoretically secure) as a function of c ddh , as otherwise the reduction to DDH would be meaningless. Indeed, the class of DDH attackers must allow for the extra resources required to run a simulation of OTP protocol in the reduction. Note also that the execution time of the global simulator is given 1:31 by S OTP and S DHKE , which are very efficient; hence the UC emulation result has a small simulation overhead [START_REF] Canetti | Universally Composable Security: A New Paradigm for Cryptographic Protocols[END_REF][START_REF] Canetti | Universally composable security: a new paradigm for cryptographic protocols[END_REF].

For the proof we used an auxiliary lemma, which is a specialization of the Universal Composability theorem for the case where the hybrid functionality is the parallel composition of two ideal functionalities and we apply the Universal Composability theorem to instantiate only one of them.

Our formalization vs EasyUC. Our Diffie-Hellman example is an alternative formalization of the example given by Canetti, Stoughton and Varia [START_REF] Canetti | EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security[END_REF] for the EasyUC framework. We borrow it because, as in [START_REF] Canetti | EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security[END_REF], it is a good toy example with which to validate and demonstrate our formalization. This example is also convenient to show that the approach in this paper and EasyUC in effect complement each other. An important design goal of EasyUC is to follow the UC execution model as closely as possible; this allows a more direct translation of protocols and ideal functionalities.

In contrast, our goal is to take advantage of the EasyCrypt machinery to reduce proof effort and development size: our development (including complexity) takes 2300 lines of code and it includes general UC theorems that can be reused in future work; this compares to 18K lines of code for EasyUC. 11 The downside of our approach is the impact in the way one specifies protocols and ideal functionalities: message passing corresponds to procedure calls, and these must adhere to the EasyCrypt tree-based procedure call semantics. For example, we do not allow an execution environment where a party communicates with an ideal functionality arbitrarily without relying on the environment for scheduling; one could of course formalize a message passing mechanism on top of EasyCrypt as in [START_REF] Canetti | EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security[END_REF] to allow for this, but this would then fall out of the scope of our general composition theorems. Moreover, it would lead to larger developments and increased proof effort, which would defeat our original purpose.

In short, one can think of the EasyUC approach as a front-end for cryptographers, and our approach as a convenient back-end for conducting the machine-checked proofs. We leave it as an interesting direction for future work to develop a sound translation between these two approaches to modeling UC for a representative class of protocols such as those considered in [START_REF] Canetti | A Simpler Variant of Universally Composable Security for Standard Multiparty Computation[END_REF]. Another interesting direction for future work is to identify UC security proofs that cannot be naturally expressed using our approach to formalizing UC and to investigate how it can be extended to deal with these examples.

RELATED WORK

Cost analysis. There is a very large body of work that uses program logics for cost analysis of imperative programs. [START_REF] Hanne | A Hoare-Like Proof System for Analysing the Computation Time of Programs[END_REF] uses Hoare logic for proving upper bounds on execution time of deterministic programs. In the probabilistic setting, [START_REF] Benjamin | Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs[END_REF] uses a pre-expectation calculus inspired from Kozen [START_REF] Kozen | A Probabilistic PDL[END_REF] and Morgan, McIver and Seidel [START_REF] Morgan | Probabilistic Predicate Transformers[END_REF] to compute upper bounds on the expected cost of probabilistic programs. Building on prior work in automation of amortized analysis, [START_REF] Van Chan Ngo | Bounded expectations: resource analysis for probabilistic programs[END_REF] develop a compositional and automated logic for proving upper bounds on expected time. Recently, [START_REF] Hark | Aiming low is harder: induction for lower bounds in probabilistic program verification[END_REF] show how the pre-expectations calculus can also be used for proving lower bounds on expected time. While most of the cryptography literature considers worst-case execution time, expected-time arises naturally in some applications; see e.g. [START_REF] Goldreich | On Expected Probabilistic Polynomial-Time Adversaries: A Suggestion for Restricted Definitions and Their Benefits[END_REF] for a discussion of expected polynomial-time in cryptography. It would be interesting to develop an adaptation of our system for expected-time complexity, based on the approach developed in [START_REF] Benjamin | Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs[END_REF]. In addition, there is a long line of work on automating cost analysis, both for deterministic and for probabilistic programs, see e.g. [START_REF] Albert | Termination and Cost Analysis with COSTA and its User Interfaces[END_REF][START_REF] Brockschmidt | Alternating Runtime and Size Complexity Analysis of Integer Programs[END_REF][START_REF] Gulwani | SPEED: Precise and Efficient Static Estimation of Program Computational Complexity[END_REF]. These techniques could be helpful to alleviate users efforts, and connecting with tools that support them is an important direction for future work.

There is also a large body of work on cost analysis of higher-order languages, both in the deterministic and probabilistic settings. Some of these works specifically focus on cryptography; e.g., [START_REF] Baillot | Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs[END_REF] develop a type system that accomodates non-heriditarily polynomial-time computations (i.e. computations that contain non-polynomial-time subroutines), and use their type system to analyze the complexity of the reduction from hardcore predicates to one-way functions. Many of these works are based on (linear) type systems [START_REF] Dal | Linear Dependent Types and Relative Completeness[END_REF][START_REF] Hoffmann | Types with Potential: Polynomial Resource Bounds via Automatic Amortized Analysis[END_REF], but other works use a fine-grained program logic to support value-dependent cost analysis [START_REF] Radicek | Monadic refinements for relational cost analysis[END_REF]. These approaches could be used in conjunction with our type-and-effect module system to support compositional reductionist proofs for a higher-order language.

Computer-aided cryptography. CryptoVerif [START_REF] Blanchet | A Computationally Sound Mechanized Prover for Security Protocols[END_REF] is an automated tool for computational security proofs. CryptoVerif uses approximate equivalences to find (or check) cryptographic reductions, and keeps track of the complexity of adversaries. Most other tools for computational security proofs, including CertiCrypt [START_REF] Barthe | Formal certification of code-based cryptographic proofs[END_REF], Foundational Cryptography Framework [START_REF] Petcher | A Mechanized Proof of Security for Searchable Symmetric Encryption[END_REF], and CryptHOL [START_REF] Basin | CryptHOL: Game-Based Proofs in Higher-Order Logic[END_REF], share their foundations and overall approach with EasyCrypt. However, these tools offer limited support for complexity reasoning and they do not support the use of modules for defining cryptographic schemes and notions. This is not a fundamental limitation, since these tools are embedded in a general-purpose proof assistant. However, extending these tools to achieve similar effects as our type-and-effect module system and program logic for complexity would represent a significant endeavor.

Our module system is inspired from EasyCrypt [START_REF] Barthe | EasyCrypt: A Tutorial[END_REF][START_REF] Barthe | Computer-Aided Security Proofs for the Working Cryptographer[END_REF]. However, the EasyCrypt module system lacks complexity restrictions, which hampers the use of compositional approaches. Beyond EasyCrypt, several other tools and approaches use structures similar to modules for formalizing cryptographic schemes and their security. Computational Indistinguishability Logic (CIL) [START_REF] Barthe | Computational indistinguishability logic[END_REF] rely on oracle systems, which are very closely related to our modules. Interestingly, the main judgment of CIL establishes the approximate equivalence of two oracle systems, and is explicitly quantified by the resources of an adversary. State-separating proofs [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF] pursue similar goals, using a notion of package. Packages have the expressivity of modules, but additionally support private functions. Our modules can emulate private functions using restrictions. At present, there is no tool support for state-separating proofs. [START_REF] Rosulek | The Joy of Cryptography[END_REF] introduces the notion of interface, which is similar to module, for formalizing cryptography.

CONCLUSION

We have developed an extension of the EasyCrypt proof assistant to support reasoning complexity claims. The extension captures reductionist statements that faithfully match the cryptographic literature and supports compositional reasoning. As a main example, we have shown how to formalize key results from Universal Composability, a long-standing goal of computer-aided cryptography. #calls

E, ρ y.д (m.f ) = #calls E, ρ y.д (s) when f-res E (m.f ) = (proc f ( ì v : ì τ ) → τ r = { _; s; _ }) #calls E, ρ y.д (ρ(x)(ì p).f )ν when f-res E (m.f ) = (abs x open)(ì p).f Note that when f-res E (m.f ) = (proc f ( ì v : ì τ ) → τ r = { _; s; _ }),
we ignore the return expression, since expression cannot contain procedure calls (only operator applications).

Intrinsic cost. The (E, ρ)-denotational semantics of an instruction s with intrinsic cost under memory ν and parameters ì

x, written i s E, ρ,ì x ν is the cost of the execution of s under ν in ρ, without counting the costs of function calls to the parameters ì

x. Formally, i _ E, ρ,ì x ν is defined exactly like _ E, ρ,ì x ν in Fig. 14, except for the abstract procedure call case, which is replaced by:

i x ← call m.f (ì e ) E, ρ,ì x ν = E (ν ′ ,c ′ )∼ i x ←call ρ(x)(ì p).f (ì e ) E, ρ, ì x ν [(ν ′ , c E (ì e, ν ))] if z ∈ ì x i x ← call ρ(x)(ì p).f (ì e ) E, ρ,ì x ν if z ì x
where f-res E (m.f ) = (abs open z)(ì p).f . Remark that both semantics coincide on their first component. Indeed, for any E-pre-interpretation ρ:

∀ν s. π # 1 ( s E, ρ ν ) = π # 1 ( i s E, ρ,ì x ν )
The (E, ρ)-intrinsic cost i-cost

E, ρ,ì x ν (_) ∈ N ∪ {+∞} of an instruction s is: i-cost E, ρ,ì x ν (s) = sup(supp(π # 2 ( i s E, ρ,ì x ν )))
The intrinsic cost of a procedure m.f , with parameters ì x, is:

• If f-res E (m.f ) = (proc f ( ì v : ì τ ) → τ r = { _; s; return r }) then: i-cost E, ρ,ì x ν (m.f ) = i-cost E, ρ,ì x ν (s) + c E (r , ν) • If f-res E (m.f ) = (abs open x)(ì p).f then: i-cost E, ρ,ì x ν (m.f ) = i-cost E, ρ,ì x ν (ρ(x)(ì p).f ) T-While Γ ⊢ e : bool Γ ⊢ s Γ ⊢ while e do s
Expressions typing Γ ⊢ e : τ .

ExprApp

type(f ) = τ 1 × • • • × τ n → τ ∀i ∈ {1; . . . ; n }, Γ ⊢ e i : τ i Γ ⊢ f (e 1 , . . . , e n ) : τ ExprVar Γ(v) = τ Γ ⊢ v : τ
Restriction entailment ⊢ θ <: θ ′ . We omit the transitivity and reflexivity rules for ⊢ θ <: θ ′ .

⊑-Proc

∀f ∈ dom(θ, θ ′ ), ⊢ θ [f ] <: θ ′ [f ] ⊢ θ <: θ ′ ⊑-Split ⊢ λ m <: λ m ′ ⊢ λ c <: λ c ′ ⊢ λ m ∧ λ c <: λ m ′ ∧ λ c ′ ⊑-Top ⊢ λ <: ⊤ ⊑-Mem λ m ⊑ λ m ′ ⊢ λ m <: λ m ′ ⊑-MemTop ⊢ λ c <: ⊤ ⊑-Compl k ≤ k ′ ∀i, k i ≤ k ′ i ⊢ compl[intr : k, x 1 .f 1 : k 1 , . . . , x n .f n : k n ] <: compl[intr : k ′ , x 1 .f 1 : k ′ 1 , . . . , x n .f n : k ′ n ] Memory restriction. mem Γ (abort) = ∅ mem Γ (skip) = ∅ mem Γ (x ← e) = {x } ⊔ vars(e) mem Γ (x $ ← -d ) = {x } mem Γ (s 1 ; s 2 ) = mem Γ (s 1 ) ⊔ mem Γ (s 1 ) mem Γ (while e do s) = vars(e) ⊔ mem Γ (s) mem Γ (if e then s 1 else s 2 ) = vars(e) ⊔ mem Γ (s 1 ) ⊔ mem Γ (s 1 ) mem Γ (x ← call p.f (ì e )) = {x } ⊔ mem Γ (p.f ) ⊔ vars(ì e ) mem Γ (p) = ⊔ f ∈procs Γ (p) mem Γ (p.f ) When f-res Γ (p.f ) = (proc f ( ì v : ì τ ) → τ r = { var ( ì v l : ì τ l ); s; return r }): mem Γ (p.f ) = (mem Γ (s) ∪ vars(r ))\{ ì v ; ì v l } When f-res Γ (p.f ) = (abs K x)(ì p 0 ).f , K = open and Γ(x) = abs K : func(_) sig _ restr θ end: mem Γ (p.f ) = θ [f ] ⊔ mem Γ (ì p 0 ) When f-res Γ (p.f ) = (abs param x)(ì p 0 ).f : mem Γ (p.f ) = mem Γ (ì p 0 )
.д skip E, ρ ν = 1 (ν , 0) y.д abort E, ρ ν = 0 y.д s 1 ; s 2 E, ρ ν = E (ν ′ ,c ′ )∼ y.д s 1 E, ρ ν [ y.д s 2 E, ρ ν ′ ⊕ c ′ ] y.д x ← e E, ρ ν = 1 (ν [x ← e ν ], 0) y.д x $ ← -d E, ρ ν = E v ∼ d ν [1 (ν [x ←v ], 0) ] y.д x ← call m.f (ì e ) E, ρ ν = let ν 0 = ν [ ì v ← ì e ν ] in E (ν ′ ,c ′ )∼ y.д s E, ρ ν 0 [1 (ν ′ [x ← r ν ′ ],c ′ ) ] (if f-res E (m.f ) = proc f ( ì v : ì τ ) → τ r = { _; s; return r }) y.д x ← call m.f (ì e ) E, ρ ν = y.д x ← call ρ(x)(ì p).f (ì e ) E, ρ ν ⊕ 1 (if f-res E (m.f ) = (
z i = ì z[i], m i = ì m[i] and M i = ì M[i] = sig _ restr λ i c ∧ _ end, 12 if: E ⊢ (module z i = m i : erase compl (M i )) and ∀д ∈ procs(M i ), cost E ν (m i .д) ≤ λ i c
(with the convention that j ≤ ⊤ for any integer j) then the execution of f in any memory verifies the complexity restriction in θ [f ]. Formally, let E ′ = E; module ì z = abs open : ì M and ρ ′ = ρ, (ì z : ì m), and:

θ [f ] = _ ∧ λ c = compl[intr : k, y 1 .f 1 : k 1 , . . . , y l .f l : k l ]
Then for every 1 ≤ j ≤ l,

#calls E ′ , ρ ′ y j .f j (x(ì z).f ) ≤ k j and i-cost E ′ , ρ ′ ,ì z (x(ì z).f ) ≤ k
Intrinsic cost of a functor. Finally, the (E, ρ)-intrinsic complexity of a functor procedure x.f , denoted by compl We give the rules for typing in already typed environment in Fig. 27. Roughly, these rules are the module expression, module structure and module environment typing rules given in Fig. 6, with the following changes:

• when typing a module declaration of a module structure, the typing environment Γ is not extended with the inferred type, as it must already be present in Γ. Consequently, we do not need to keep track of the current path of the sub-module expression being typed, which simplifies the rules. • we added a rule for abstract modules, for the application of a module expression to a module path, and for component access. This allows to type the intermediate terms that appear during the module resolution procedure. • when typing an environment, the typing environment is not extended with the inferred types. Before going further, we give the definition of well-formed typing environments. Essentially, a typing environment Γ is well-formed if it contains no duplicate declarations, and it contains only well-formed module signature.

Definition C.2. A typing environment Γ is well-formed iff:

• whenever Γ = (Γ 0 ; Decl z ; Γ 1 ) then (Γ 0 ; Γ 1 )(z) undef , where:

Decl z ∈ module z = m : M; var z : τ ; proc z( ì v : ì τ ) → τ r
Finally, cost judgment E ⊢ {ϕ} F {ψ | t } on function path have the same semantics than cost judgment on statements, i.e. for every well-typed environment E, for every E-interpretation ρ and ν ∈ ϕ:

supp(π # 1 ( F E, ρ ν )) ⊆ ψ ∧ cost E, ρ ν (F) ≤ t[conc] + A∈abs(E)f ∈procs(E(A)) t[A.f ] • compl E, ρ A.f (5)

D.1 Abstract Call Rule Soundness

We now prove that the abstract call rule Abs in Fig. 12 is sound. First, remark that since the rule Abs uses a different upper-bound t H.д (k) on the cost of the k-th call to the oracle H.д, and since the fact that we are in the k-th call is characterized by the invariant I , we must prove both properties (the invariant on the memories, and the upper-bound on the complexity of the call) simultaneously. The proofs is by induction on the size in E of the procedure ρ(x).f called, where procedure calls are inlined. Formally, for every environment E and E-pre-interpretation ρ, we define:

#size E ρ (abort) = 1 #size E ρ (skip) = 1 #size E ρ (s 1 ; s 2 ) = 1 + #size E ρ (s 1 ) + #size E ρ (s 2 ) #size E ρ (x ← e) = 1 = 1 #size E ρ (x $ ← -d) = 1 = 1 #size E ρ (x ← call F(ì e )) = 1 + #size E ρ (s) ( if f-res E (F) = proc f _ = { _; s; _ }) #size E ρ (x ← call F(ì e )) = 1 + #size E ρ (x ← call ρ(x)(ì p).f (ì e )) ( if f-res E (F) = (abs open x)(ì p).f ) #size E ρ (if e then s 1 else s 2 ) = 1 + #size E ρ (s 1 ) + #size E ρ (s 2 )
#size E ρ (while e do s) = 1 + #size E ρ (s)

Note that we do not care about the size of the expressions appearing in the statement. We now define and prove our (generalized) induction property, which we need to prove the soundness of Abs after. Lemma D.1. Let I a formula, E a well-typed environment, ρ an E-interpretation and ì

x be functor parameters with module types abs open ì M which are module structure signatures (i.e. not functors). For every statement s well-typed in E with additional functor parameters abs param ì

x : ì M, and satisfying a memory restriction λ s m :

Γ ⊢ s Γ ⊢ s ▷ λ s m where Γ = E, module ì x = abs param : ì M
Then for every valuation ì p of the parameters ì x well-typed in E (i.e. E ⊢ ì p : ì M), if we let E ′ = E, module ì

x = abs open : ì M, and ì O be an enumeration of the parameters ì x's procedures, i.e. of:

y.h | y ∈ ì x ∧ h ∈ procs( ì M[y])
Then if:

• the memory of the statement s is independent of I , except for calls to the parameters ì x, i.e.:

λ s m ∩ FV(I ) = ∅
• for every parameters' procedure H.д ∈ procs Γ (ì x), the k-th call to H.д (when H is instantiated by ì p[H]) preserves the invariant and has a cost upper-bounded by t

H.д [k] (for k ≤ λ c [H.д]): ∀ ì k ≤ λ c [ ì O], ì k[H.д] < λ c [H.д] → E ⊢ {I ì k} ì p[H].f {I ( ì k + 1 H.д ) | t H.д ( ì k[H.д])} (6)
• the number of calls from s to the parameters' procedure is upper-bounded by λ c [ ì O] -ì k (for memory satisfying the invariant I ì k):

∀ ì k ≤ λ c [ ì O], ∀ν ∈ I ì k, ∀H.д ∈ procs E (ì x), #calls E ′ , ρ ′ H.д,ν (s) ≤ λ c [H.д] -ì k[H.д] (7)
For every H.д ∈ procs E (ì x) and j < λ c [H.д], we define:

call-cost E, ρ H.д (j) = t H.д (j)[conc] + A∈abs(E) f ∈procs E (A) t H.д (j)[A.f ] • compl E, ρ A.f Let ρ ′ = ρ, (ì x : ì p). We have that for every ì k ≤ λ c [ ì O] and ν ∈ I ì k: supp(π # 1 ( s E ′ , ρ ′ ν )) ⊆ I ( ì k + #calls E ′ , ρ ′ ì O,ν (s)) (8)
and:

cost E ′ , ρ ′ ν (s) ≤ i-cost E ′ , ρ ′ ,ì x ν (s) + H.д ∈procs E (ì x) ì k [H.д]+#calls E ′ , ρ ′ H.д,ν (s)-1 j= ì k [H.д] call-cost E, ρ H.д (j) (9)
That is, the cost of s executed in E ′ , ρ ′ and memory ν (satisfying the invariant I ì k) is upperbounded by the intrinsic cost of s with functors parameters ì

x, of the sum over functor parameters' procedures H.д ∈ procs E (ì x) of the sum over all calls to H.д (which ranges from ì k

[H.д] to #calls E ′ , ρ ′
H.д,ν (s) -1) of the concrete cost of (the j-th call to) H.д (upper-bounded by t H.д (j)[conc]), plus the sum, over all abstract procedures A.f (in the original environment E), of the number of times the j-th call to H.д called A.f (upper-bounded by t H.д (j)[A.f ]) times the maximal cost of A.f (which is compl

E, ρ A.f ).
Proof. We prove this induction over #size E ρ (s). We do a case analysis on s:

• if s is abort or skip, this is immediate. • if s = s 1 ; s 2 . Let ì k ≤ λ c [ ì O] and ν ∈ I ì k. We know that: supp(π # 1 ( s 1 ; s 2 E ′ , ρ ′ ν )) = ν ′ ∈supp(π # 1 ( s 1 E ′ , ρ ′ ν )) supp(π # 1 ( s 2 E ′ , ρ ′ ν ′ )) Let ì k 1 = ì k + #calls E ′ , ρ ′ ì O,ν (s 1 ). By induction hypothesis applied on s 1 , supp(π # 1 ( s 1 E ′ , ρ ′ ν )) ⊆ I ì k 1 (10) Let ν ′ ∈ supp(π # 1 ( s 1 E ′ , ρ ′ ν )), we know that ì k 1 ≤ λ c [ ì O].
Hence, by induction hypothesis on s 2 , we deduce that:

supp(π # 1 ( s 2 E ′ , ρ ′ ν ′ )) ⊆ I ì k 2 where ì k 2 (ν ′ ) = ì k + #calls E ′ , ρ ′ ì O,ν (s 1 ) + #calls E ′ , ρ ′ ì O,ν ′ (s 2 ). Since: #calls E ′ , ρ ′ ì O,ν (s 1 ) + #calls E ′ , ρ ′ ì O,ν ′ (s 2 ) ≤ #calls E ′ , ρ ′ ì O,ν (s 1 ; s 2 ) (11)
we deduce: supp

(π # 1 ( s 2 E ′ , ρ ′ ν ′ )) ⊆ I ( ì k + #calls E ′ , ρ ′ ì O,ν (s 1 ; s 2 ))
which concludes the proofs of the first point. It remains to prove that the complexity of s 1 ; s 2 is upper-bounded by the wanted quantity. First, we have:

cost E ′ , ρ ′ ν (s 1 ; s 2 ) = cost E ′ , ρ ′ ν (s 1 ) + max ν ′ ∈supp(π # 1 ( s 1 E ′ , ρ ′ ν )) cost E ′ , ρ ′ ν ′ (s 2 )
By applying the induction hypothesis on s 1 and s 2 with, respectively, ì k and ì k 1 , we get:

cost E ′ , ρ ′ ν (s 1 ) ≤ i-cost E ′ , ρ ′ ,ì x ν (s 1 ) + H.д ∈procs E (ì x) ì k 1 [H.д]-1 j= ì k [H.д] call-cost E, ρ H.д (j)
and:

cost E ′ , ρ ′ ν ′ (s 2 ) ≤ i-cost E ′ , ρ ′ ,ì x ν ′ (s 2 ) + H.д ∈procs E (ì x) ì k 2 (ν ′ )[H.д]-1 j= ì k 1 [H.д] call-cost E, ρ H.д (j) Since i-cost E ′ , ρ ′ ν (s 1 ; s 2 ) is equal to: i-cost E ′ , ρ ′ ν (s 1 ) + max ν ′ ∈supp(π # 1 ( s 1 E ′ , ρ ′ ν )) i-cost E ′ , ρ ′ ν ′ (s 2 )
and using Equ. [START_REF] Barthe | Computer-Aided Security Proofs for the Working Cryptographer[END_REF], we deduce that:

cost E ′ , ρ ′ ν (s 1 ) + cost E ′ , ρ ′ ν ′ (s 2 ) ≤ i-cost E ′ , ρ ′ ν (s 1 ; s 2 ) + H.д ∈procs E (ì x) ì k [H.д]+#calls E ′ , ρ ′ ì O,ν (s 1 ;s 2 )-1 j= ì k[H.д] call-cost E, ρ H.д (j)
We conclude by taking the max over ν ′ and using Equ. 10.

• if s = x ← e. Let ì k ≤ λ c [ ì O] and ν ∈ I ì k.
Since mem Γ (s) ∩ FV(I ) = ∅, we know that x FV(I ). Hence the invariant is preserved, i.e.:

∀ν ′ ∈ supp(π # 1 ( s E ′ , ρ ′ ν ))), ν ′ ∈ I ì k Since #calls E ′ , ρ ′ ì O,ν (s)
= 0, this proves the first point. Moreover:

cost E ′ , ρ ′ ν (x ← e) = i-cost E ′ , ρ ′ ,ì x ν (x ← e)
which concludes the proof. • the random assignment x $ ←d, conditional if e then s 1 else s 2 and while loop while e do s cases are similar. We omit the details.

• if s = x ← call F(ì e ) and f-res E (F) = (proc f ( ì v : ì τ ) → τ r = { var ( ì v l : ì τ l ); s ′
; return e }), then we proceed as in the previous case, applying the induction hypothesis on s ′ . First, we remark that s ′ is smaller than s, since:

#size E ρ (s ′ ) < #size E ρ (x ← call F(ì e ))
It only remains to check that the induction hypothesis's hypotheses hold. The last two hypotheses are straightforward to show. It only remains to prove that Γ ⊢ s ′ ▷ λ s m is derivable. Since Γ ⊢ s ▷ λ s m , we know that mem Γ (s) ⊆ λ s m , where:

mem Γ (s) = {x } ⊔ mem Γ (s ′ ) ⊔ vars(ì e ) 1:53 Which concludes this case. • idem if s = x ← call F(ì e ) and f-res E (F) = (abs open H)(_).f with H ì x. • if s = x ← call F(ì e ) and f-res E (F) = (abs open H)(ì p ′ ).д with H ∈ ì
x, then we use the hypothesis that procedures of the interpretation of the modules parameters ì

x preserves the invariant.

First, since ì x have types ì M and ì M are module structure signatures, we know that ì p ′ is empty (from the fact that s is well-typed in Γ). Hence f-res

E (F) = abs open H.д. Let ì k ≤ λ c [ ì O] and ν ∈ I ì k.
First, using the hypothesis in Eq. ( 7), we know that:

ì k[H.д] + #calls E ′ , ρ ′ H.д,ν (x ← call F(ì e)) ≤ λ c [H.д] Hence ì k[H.д] < λ c [H.д]
. By applying Equ. ( 6) on H.д, we know that:

E ⊢ {I ì k} ì p[H].д {I ( ì k + 1 H.д ) | t H.д (k)} (12)
Since ρ is an E-interpretation, and since ì x have type ì M where ì M are module structure signatures, we can check that ρ ′ is an E ′ -interpretation. Hence, from Equ. ( 12) and the semantics of the cost judgment given in Equ. [START_REF] Barbosa | SoK: Computer-Aided Cryptography[END_REF] we get that:

supp(π # 1 ( ì p[H].д E, ρ ν )) ⊆ I ( ì k + 1 H.д ) (13) and: cost
E, ρ ν (ì p[H].д) ≤ t H.д ( ì k[H.д])[conc] + A∈abs(E) f ∈procs E (A) t H.д ( ì k[H.д])[A.f ] • compl E, ρ A.f ≤ call-cost E, ρ H.д ( ì k[H.д]) (14)
Observe that since ρ ′ = ρ, (ì x : ì p), we have:

x ← call F(ì e ) E ′ , ρ ′ ν = x ← call ì p[H].д(ì e ) E ′ , ρ ′ ν
Hence Equ. (8) follows directly from Equ. [START_REF] Bellare | Random Oracles are Practical: A Paradigm for Designing Efficient Protocols[END_REF]. It remains to show Equ. [START_REF] Barthe | A Program Logic for Union Bounds[END_REF]. First, note that:

cost E ′ , ρ ′ ν (x ← call F(ì e )) = i-cost E ′ , ρ ′ ,ì x ν (x ← call F(ì e )) + cost E ′ , ρ ′ ν (ì p[H].д)
Since ì p is well-typed in E, we know that cost We conclude the proof of Equ. (9) using the inequality above and Equ. [START_REF] Blanchet | A Computationally Sound Mechanized Prover for Security Protocols[END_REF]. □ Lemma D.2. The rule Abs given in Fig. 12 is sound.

Proof. We just apply Lemma D.1 on ρ(x).f . The first two hypotheses of the lemma hold thanks to the premises of the Abs rule, and using the fact our module system has the subject reduction property (Lemma C.1). The third hypothesis follows from the fact that ρ is an E-interpretation. □

D.2 Instantiation Rule Soundness

We prove the following technical lemma, which allows to extend an E-interpretation ρ into an (E, module x = abs open : M l )-interpretation ρ ′ = ρ, (x → m). This is possible whenever: i) m has type erase compl (M l ); ii) and we can show that m verifies M l 's complexity restriction by proving that:

M ⊢ {⊤} m(ì x).f {⊤ | t f } ∧ t f ≤ compl θ [f ] (15)
then ρ a = ρ, (x → m) is an E a -interpretation. Moreover, for any f ∈ procs(M l ): ). To prove that ρ a is an E a -interpretation, we only need to prove that:

compl E a , ρ a x.f ≤ t f [conc] + A∈abs(E) h ∈procs E (A) t f [A.h] • compl E, ρ A.h
#calls

E ′ a , ρ ′ a y.д (x(ì x).f ) ≤ θ [f ][y.д] (17)
and that:

i-cost E ′ a , ρ ′ a ,ì x (x(ì x).f ) ≤ θ [f ][intr] (18)
Restriction to module structures. First, note that w.l.o.g. we can assume that ì m are all module structure (i.e. of the form struct _ end). Basically, we show that we can build another interpretation ρ ′′ a extending ρ a which satisfies the same hypotheses than ρ ′ a , and such that for every z ∈ ì x, ρ ′′ a (z) is a module structure such that, for every д ∈ procs( ì M[z]):

#calls

E ′ a , ρ ′
where: Since E is well-typed, and ì m have types ì M in E, and since ì M is not a functor type, we can check that E ′ is well-typed, and ρ ′ is an E ′ -interpretation. Using Equ. [START_REF] Brockschmidt | Alternating Runtime and Size Complexity Analysis of Integer Programs[END_REF], we get:

E ′ = E;
∀ν, cost E ′ , ρ ′ ν (m(ì x).f ) ≤ t f [conc] + A∈abs(E ′ ) h ∈procs E ′ (A) t f [A.h] • compl E ′ , ρ ′ A.h (20)
Let N > 0 be an non-zero positive integer. We are going to change the interpretation of y in ρ ′ by adding some code doing nothing and taking time N . Let st y be such that ρ ′ (y) = struct st y end. By typing hypothesis, we know that st y is of the shape: Let ν be some arbitrary memory. Since ρ ′ is an E ′ -interpretation, then so is ρ ′ N . Using Equ. (15), we get: This, together with Equ. [START_REF] Canetti | Universally composable security: a new paradigm for cryptographic protocols[END_REF], proves Equ. [START_REF] Canetti | Universally Composable Security: A New Paradigm for Cryptographic Protocols[END_REF] Finally, to prove that Equ. [START_REF] Canetti | Universally Composable Security: A New Paradigm for Cryptographic Protocols[END_REF] and Equ. 16 hold we do the exactly the same reasoning, this time by adding to the interpretation of x some code doing nothing and taking time N . □

cost E ′ , ρ ′ N ν (m(ì x).f ) ≤ t f [conc] + A∈abs(E ′ ) h ∈procs E ′ (A) t f [A.h] • compl E ′ , ρ ′ N A.h
We also prove the following weakening lemma for the intrinsic complexity of a procedure. and compl E, ρ

x.f ≥ compl E 1 , ρ 1

x.f . The latter inequality is straightforward to show, since any E ′ 1 -interpretation ρ 1 can be extended into an E ′ -interpretation ρ that leaves the intrinsic cost of x unchanged, i.e. such that for any ν :

i-cost E ′ , ρ ′ ,ì x ν (x(ì x).f ) = i-cost E ′ 1 , ρ ′ 1 ,ì x ν (x(ì x).f )
To prove the former inequality, we show that any E ′ -interpretation ρ can be transformed into an E ′ 1 -interpretation ρ ′ such that Equ. (D.2) holds, by inlining all modules of E 2 in ρ. We omit the details. □ Lemma D.5. The rule Instantiation given in Fig. 13 is sound.

Proof. We consider an instance of the rule Instantiation. We want to prove that: We know that M l = func(ì y : ì M) sig S l restr θ end and:

E a ⊢ {ϕ} s {ψ | t s } (24)
Using Lemma D.3, we know that ρ a = ρ, (x → m) is an E a -interpretation. Hence, using Equ. ( 24 Which, by definition of T ins , is exactly Equ. [START_REF]Source code of our EasyCrypt[END_REF]. □

Fig. 1 .

 1 Fig. 1. Example of an EasyCrypt module.

Fig. 2 .

 2 Fig. 2. Inverter for trapdoor permutation in EasyCrypt.

Fig. 3 .

 3 Fig. 3. Program and module syntax

  Signature structures (for any n ∈ N): S ::= D 1 ; . . . ; D n Module signature declarations: D ::= proc f ( ì v : ì τ ) → τ r | module x : M Module signatures: M ::= sig S restr θ end | func(x : M) M ′

Fig. 4 .

 4 Fig. 4. Module signatures and restrictions

  module type HSM = { proc enc (x:msg) : cipher }. module Hsm : HSM = { proc enc (x:msg) : cipher = { . . . } }. module type Adv (H : HSM) {+all mem, -Hsm} = { proc guess () : skey compl[intr : k 0 , H.enc : k]}.

Fig. 5 .

 5 Fig. 5. Example of adversary with restrictions.

  Fig. 7. Example: valid and invalid paths.

3

 3

Abstract modules.

  Abstract modules representing open code (i.e. with kind open) are restricted to low-order signatures: M l ::= sig S l restr θ end | func(x : sig S l restr θ end) M l S l ::= D l1 ; . . . ; D ln D l ::

Fig. 8 .

 8 Fig. 8. Restriction checking rules.

  module type T C = { proc c () : unit }. module C = { proc c () = { s c } }. module type T B (C 0 : T C ) = { proc b () : unit compl[intr : t b , C 0 .c : 2] }. module type T A (B 0 : T B ) (C 0 : T C ) = { proc a () : unit compl[intr : t a , B 0 .b : 1, C 0 .c : 1] }. module A (B 0 : T B ) (C 0 : T C ) : T A = { proc a () = { s 1 ; C 0 .c(); s 2 ; B 0 (C 0 ).b(); s 3 ; }}. Judgment E ⊢ {⊤} A(B, C).a {⊤ | [conc → t conc , B.b → 1]} where E = (module B = abs open : T B ).

Fig. 10 .

 10 Fig. 10. Graphical representation of the different cost measurements.

Example 4 . 1 .

 41 Consider E with two abstract modules x and y: E = (module x = abs open : sig (proc f _) restr _ end); (module y = abs open : sig (proc h _) restr _ end)

Fig. 11 .

 11 Fig. 11. Basic rules for cost judgment.

Fig. 13 .

 13 Fig. 13. Instantiation rule for cost judgment.

Fig. 14 .

 14 Fig. 14. (E, ρ)-denotational semantics _ E, ρ ν .

Definition 5 . 2 .

 52 the judgment ⊢ {ϕ} e ≤ t e stands for: ∀ν ∈ ϕ, c E (e, ν) ≤ t e Definition 5.3. The judgment E ⊢ {ϕ} s {ψ | t } means that for any E-interpretation ρ and ν ∈ ϕ:

Theorem 5 . 1 .

 51 The proof rules inFigures 12,[START_REF] Barthe | Computer-Aided Security Proofs for the Working Cryptographer[END_REF] and 13 are sound. The proof can be found in Appendix D ACM Trans. Priv. Sec., Vol. 1, No. 1, Article 1. Publication date: March 2023.

1 : 23

 123 module type IO = { proc inputs (i:inputs) : unit proc outputs(o:ask_outputs) : outputs option }. module type BACKDOORS = { proc step (m:step) : unit proc backdoor (m:ask_backdoor) : backdoor option }. module type E_INTERFACE = { include IO include BACKDOORS }. module type PROTOCOL = { proc init() : unit include E_INTERFACE }.

Fig. 15 .

 15 Fig. 15. PROTOCOL type in EasyCrypt.

module

  UC_emul (E:ENV) (P:PROTOCOL) = { proc main() = { var b; P.init(); b ← E(P).distinguish(); return b; } }. module CompS(F:IDEAL.PROTOCOL, S:SIMULATOR) : PROTOCOL = { proc init() = { F.init(); S(F).init(); } include F [ inputs, outputs] include S(F) [step, backdoor] }.

Fig. 16 .

 16 Fig. 16. Execution model for real/ideal worlds (top) and composition of functionality with a simulator (bottom).

Fig. 17 .

 17 Fig. 17. Module restrictions. Arrows indicate ability to make procedure calls via the interface specified as a label; all other cross-boundary memory access is disallowed.

1 : 27 becomeFig. 18 .

 12718 Fig. 18. Real-world protocol with adversary.

Fig. 22 .

 22 Fig. 22. Memory restriction operations and type erasure functions.

Fig. 23 .

 23 Fig. 23. Additional typing rules and operations.

  y

Fig. 26 .

 26 Fig. 26. Function call counting semantics y.д _ E, ρ ν .

  ∈ N ∪ {+∞}, is the maximal intrinsic cost of x.f 's body over all possible memories and instantiation of x's functor parameters. Let E(x) = abs open (func(ì z : ì M) sig _ end)and E ′ = (E; module ì z = abs open : ì M). Also, let I be the set E ′ -interpretation ρ ′ extending ρ. Then:compl E, ρ x.f = sup ρ ′ ∈I i-cost E ′ , ρ ′ ,ì z (x(ì z).f )performing the application. Consequently, we can have intermediate expressions of the form m(p).Similarly, when resolving a module component access p.x, we first resolve p into a module structure and then access its component x. This yields intermediate expressions of the form m.x.Example C.2. We recall Example 3.1 which we presented in Section 3. We recall that Γ is a typing environment Γ such that:Γ(x) = struct module y = func(u : _) u end Γ(z) = abs open z Γ(v) = m v Γ(w) = abs param wwhere m v is some module expression. The resolution of the module expression x.y(z)(v)(w) in Γ is as follows:x.y(z)(v)(w)⇒ res. step struct module y = func(u : _) u end .y(z)(v)(w)⇒ res. step func(u : _) u (z)(v)(w) ⇒ res. step z(v)(w) ⇒ res. step (abs open z)(v)(w) ⇒ res. step ((abs open z)(v))(w) ⇒ res. step (abs open z)(v, w)Therefore, to prove subject reduction for the module resolution procedure, we consider an extended syntax for modules (and add the corresponding typing rules). Definition C.1. A partially resolved module expression m is an element of the form: m ::= m | m(p) | m.x It is enough to allow only top-level applications of module expressions to module paths and module component accesses.

E

  ′ , ρ ′ ν (ì p[H].д) = cost E, ρ ν (ì p[H].д). Hence: cost E ′ , ρ ′ ν (x ← call F(ì e )) = i-cost E ′ , ρ ′ ,ì x ν (x ← call F(ì e )) + cost E, ρ ν (ì p[H].д)

  ∀f ∈ procs(M l ), E, module ì x = abs open : ì M ⊢ {⊤} m(ì x).f {⊤ | t f } where ì x are M l 's functor parameters, and ì M their types. Lemma D.3. Let E be a well-typed environment, M l be low-order module signature s.t.: M l = func(ì x : ì M) sig _ restr θ end and m be a module expression s.t. E ⊢ x m : erase compl (M l ). Let E a = E, module x = abs open : M l and ρ be an E-interpretation. If, for every f ∈ procs(M l ), we have: E, module ì x = abs open : ì

  ì m be an evaluation of x's parameters s.t. for every 1≤ i ≤ |ì x|, if we let x i = ì x[i], m i = ì m[i] and M i = ì M[i] = sig _ restr λ i c ∧ _ end: E ⊢ (module x i = m i : erase compl (M i ))and:∀д ∈ procs(M i ), cost E ν (m i .д) ≤ λ i c Let E ′ a = E a ; module ì x =abs open : ì M and ρ ′ a = ρ a , (ì x : ì m). Also, let y ∈ ì x and д ∈ procs( ì M[y]

  E ′ a , ρ ′ a ,ì x (x(ì x).f ) = i-cost E ′ a , ρ ′′ a ,ì x (x(ì x).f )Indeed, assume that there exists some y ∈ ìx such that ì m[y] is not a module structure in ρ ′ a . If ì m[y] is a module path p in ρ ′a , then we resolve it in E, ρ (which is always possible, since ì m[y] is well-typed in E and ρ is an E-interpretation) until we get a module structure struct st end, and replace y by struct st end in ρ ′′ a . Finally, ì m[y] cannot be a functor (by typing hypothesis) in ρ ′ a . We repeat the steps above until (ρ ′ a )[ì x] are all module structures.

  Proof of Equ.[START_REF] Canetti | Universally Composable Security: A New Paradigm for Cryptographic Protocols[END_REF]. Since ρ ′ a (x) = m and m is well-typed in E, and since the module expressions ì m are well-typed in E, we can removed x from the environment and the interpretation while keeping the semantics unchanged. That is, we have:#calls E ′ a , ρ ′ a y.д (x(ì x).f ) = #calls E ′ , ρ ′y.д (m(ì x).f )

  module ì x = abs open : ì M and ρ ′ = ρ, (ì x : ì m)

st y = st 1 ;

 1 proc д( ì v : ì τ ) → τ r = { var ( ì v l : ì τ l ); s д ; return e д }; st 2Then, we let st N y be the module structure:st 1 ; proc д( ì v : ì τ ) → τ r = { var ( ì v l : ì τ l ); (tic N ; s д ); return e д }; st 2and let ρ ′ N be the interpretation with the same domain as ρ ′ s.t.:∀w ∈ dom(ρ ′ ), ρ ′ N (w) = ρ ′ (w) if w y struct st N y end if w = y

  can easily check that:#calls E ′ , ρ ′ y.д (m(ì x).f ) = #calls E ′ , ρ ′ N y.д (m(ì x).f ) and: cost E ′ , ρ ′ N ν (m(ì x).f ) = cost E ′ , ρ ′ ν (m(ì x).f ) + N • #calls E ′ , ρ ′ y.д (m(ì x).f )From Equ.[START_REF] Canetti | EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security[END_REF], we have:cost E ′ , ρ ′ ν (m(ì x).f ) + N • #calls E ′ , ρ ′ y.д (m(ì x).f ) ≤ t f [conc] + A∈abs(E ′ ) h ∈procs E ′ (A) t f [A.h] • compl E ′ , ρ ′N A.h ACM Trans. Priv. Sec., Vol. 1, No. 1, Article 1. Publication date: March 2023.Using the inequality above, and Equ.[START_REF] Canetti | A Simpler Variant of Universally Composable Security for Standard Multiparty Computation[END_REF], we have:N • #calls E ′ , ρ ′ y.д (m(ì x).f ) ≤ A∈abs(E ′ ) h ∈procs E ′ (A) t f [A.h] • (compl E ′ , ρ ′ N A.h -compl E ′ , ρ ′ A.h ) ≤ t f [y.д] • (compl E ′ , ρ ′ N y.д -compl E ′ , ρ ′ y.д ) (Since ∀z y, ρ ′ N (z) = ρ ′ (z)) ≤ t f [y.д] • N We deduce that #calls E ′ , ρ ′ y.д (m(ì x).f ) ≤ t f [y.д]. From Equ. (15), we get that:#callsE ′ , ρ ′ y.д (m(ì x).f ) ≤ θ [f ][y.д]

Lemma D. 4 .

 4 For every well-typed environment E, if:E = E 1 ; E 2 where E 1 = E 0 ; module x = abs open : M land E 2 contains only module declarations. Then for every f ∈ procs(M l ) and E-interpretation ρ, we have complE, ρ x.f = compl E 1 , ρ 1 x.fwhere ρ 1 is the restriction of ρ to E 1 's abstract modules. Proof sketch. Assume M l = (func(ì x : ì M) sig _ end). Let E ′ = (E, module ì x = abs open : ì M) and E ′ 1 = (E 1 , module ì x = abs open : ì M), we prove that compl E, ρ x.f ≤ compl E 1 , ρ 1 x.f

  E, module x = m : M l ⊢ {ϕ} s {ψ | T ins } Let E c = (E, module x = m : M l ) and E a = (E, module x = abs open : M l ). We know that:M l = func(ì y : ì M) sig S l restr θ end E ⊢ x m : erase compl (M l )Let ρ be an E c -interpretation and ν ∈ ϕ, we need to show that for every memory ν :supp(π # 1 ( s E c , ρ ν )) ⊆ ψ (22) cost E c , ρ ν (s) ≤ T ins [conc] + A∈abs(E c ) д ∈procs Ec (A) T ins [A.д] • compl E c , ρ A.д(23)ACM Trans. Priv. Sec., Vol. 1, No. 1, Article 1. Publication date: March 2023. Mechanized Proofs of Adversarial Complexity and Application to Universal Composability Journal pre-print: full version 1:57

  intr E (A.h) is the upper-bound on A.h intrinsic cost declared in E (if A.h declares no intrinsic bound in E, then intr E (A.h) is undefined (hence A.h execution time can be arbitrarily large), and the Instantiation rule cannot be applied). In other words, the concrete execution time t f [conc] of x.f , plus the abstract execution time of x.f (excluding functor parameters, already accounted for), must be bounded by θ [f ][intr].

1, No. 1, Article 1. Publication date: March 2023.

where

  Using the fact that ρ a (x) = m, we can check (by induction over #size From the left equality above and Equ.[START_REF] Gulwani | SPEED: Precise and Efficient Static Estimation of Program Computational Complexity[END_REF], we know that Equ.[START_REF] Dal | Linear Dependent Types and Relative Completeness[END_REF] holds. It remains to prove Equ.[START_REF]Source code of our EasyCrypt[END_REF].From the right equality above and Equ.[START_REF] Haagh | Computer-Aided Proofs for Multiparty Computation with Active Security[END_REF]:cost A∈abs(E a ) д ∈procs Ea (A) t s [A.д] • compl E a , ρ a A.д ≤ t s [conc] + f ∈procs(S l ) t s [x.f ] • complA.д for every A ∈ abs(E c ) and д ∈ procs E c (A) using Lemma D.4:We check that the quantities above are identical when evaluated in E c , hence: complE a , ρ a x.f ≤ t f [conc] + A∈abs(E c )Hence, re-organizing the terms in the sum in Equ. (27):

									),
	we deduce that:
									supp(π # 1 ( s	E a , ρ a ν	)) ⊆ ψ	(25)
				cost ν E a , ρ a	(s) ≤ t s [conc] +	t s [A.д] • compl A.д E a , ρ a	(26)
									A∈abs(E a ) д ∈procs Ea (A)
									ρ a E a (s)) that:
		s	E a , ρ a ν	= s	E c , ρ ν		and	cost ν E a , ρ a	(s) = cost ν E c , ρ	(s)
									E a , ρ a
									x.f
									+	E a , ρ a A.д t s [A.д] • compl
									A∈abs(E c ) д ∈procs Ec (A)
	We replace compl A.д E a , ρ a	by compl	E c , ρ
				cost ν E c , ρ	(s) ≤ t s [conc] +	E a , ρ a x.f t s [x.f ] • compl
									f ∈procs(S l )
									+	t s [A.д] • compl A.д E c , ρ	(27)
									A∈abs(E c ) д ∈procs Ec (A)
	Using Lemma D.3, we upper-bound compl x.f E a , ρ a	for every f ∈ procs(S l ):
				compl x.f E a , ρ a	≤ t f [conc] + A∈abs(E) д ∈procs E (A)	E, ρ A.д t f [A.д] • compl
									д ∈procs Ec (A)	E c , ρ A.д t f [A.д] • compl
	cost ν E c , ρ	(s) ≤ t s [conc] +			t s [x.f ] • t f [conc]+
						f ∈procs(S l )

E c , ρ ν (s) ≤ t s [conc] + A∈abs(E c )д ∈procs Ec (A) t s [A.д] + f ∈procs(S l ) t s [x.f ] • t f [A.д] • compl E c , ρ A.д

ACM Trans. Priv. Sec., Vol. 1, No. 1, Article 1. Publication date: March 2023.

Meaning that the (variable, module or procedure) path z is not declared by Γ, even through a sub-module or functor application. ACM Trans. Priv. Sec., Vol. 1, No. 1, Article 1. Publication date: March 2023.

If the rule forced to take ϕ = ψ [x ← e], then it would not be complete, as prior information on the value on x (e.g. coming from a previous assignment to x ) is erased, which may prevent us from proving a precise upper-bound on ⊢ {ϕ } e ≤ t e . ACM Trans. Priv. Sec., Vol. 1, No. 1, Article 1. Publication date: March 2023.

Some of our lemmas do not hold if all programs have a cost of zero.

Intuitively, the UC model expresses a single line of execution using a token-passing mechanism that allows one machine to transfer computational resources to another, and even to create new machines. In our setting, resource analysis is much simpler. All modules representing honest and adversarial entities are fixed from the start and the cost model is concrete: all adversarial entities have a resource usage type, which means they are known to execute a maximum number of operations and perform a bounded number of procedure calls. Hence the resources used by any subset of modules in our formalizations can be stated as expressions over these type parameters. ACM Trans. Priv. Sec., Vol. 1, No. 1, Article 1. Publication date: March 2023.

Ideal-world backdoors are used to weaken the security requirements and are usually tailored to bring the security definition down to a level that can be met by real-world protocols. Note that the definition of meaningful ideal functionalities is a crucial aspect of UC security theory; here we just provide a mechanism that permits formalizing such definitions in EasyCrypt.

Real-world settings using ideal functionalities as sub-components are called hybrid.

The emulation notions in[START_REF] Canetti | Universally Composable Security: A New Paradigm for Cryptographic Protocols[END_REF][START_REF] Canetti | Universally Composable Security: A New Paradigm for Cryptographic Protocols[END_REF] quantify over a restricted class of balanced environments. Intuitively, such environments must be fair to the simulator in that polynomial-time execution in the size of its inputs is comparable to the execution time of the real-world adversary. Without this restriction, the definition would require the existence of a simulator that uses much less resources than the real-world attacker, which makes the definition too strong. Balanced environments guarantee that the resources given to the simulator match those given to the real-world adversary; moreover, the dummy adversary is formally explicit in the real-world to enable this resource accounting. In our setting we deal with this issue differently: the EasyCrypt resource model is concrete, which means that one can explicitly state in the security definition which resources are used by the simulator and assess what this means in terms of protocol security. We refer the interested reader to[START_REF] Canetti | Universally Composable Security: A New Paradigm for Cryptographic Protocols[END_REF] Section 4.4] for a discussion of quantitative UC definitions such as the one we adopt. For this reason, as we show below, we also do not need to keep the dummy adversary explicitly in the real world. ACM Trans. Priv. Sec., Vol. 1, No. 1, Article 1. Publication date: March 2023.

For this reason the simulator is often called an ideal world adversary; we do not adopt this terminology here to avoid confusion. The order of the quantifiers in the emulation definition is crucial for its compositional properties: it requires that, for all adversaries A, there exists a simulator S such that, for all environments Z, the real-and ideal-worlds are indistinguishable. We now show that the same result holds in our setting. ACM Trans. Priv. Sec., Vol. 1, No. 1, Article 1. Publication date: March 2023.

The count excludes general purpose libraries, but we should note that the exact numbers are not important, as the size of a development varies significantly with style of coding and the use of automation. ACM Trans. Priv. Sec., Vol. 1, No. 1, Article 1. Publication date: March 2023.

Γ(p.f ) = (proc f ( ì v : ì τ ) → τ r = _) Γ ⊢ p.f : (proc f ( ì v : ì τ ) → τ r ) T-If Γ ⊢ e : bool Γ ⊢ s 1 Γ ⊢ s 2 Γ ⊢ if e then s 1 else s 2

Indeed, since M l is a low-order signature, M i must be a module structure signature.

Γ ⊩ struct st end : sig S restr θ endD-Func Γ ⊢ M 0 Γ(x) undef Γ, module x = abs param : M 0 ⊩ m : M Γ ⊩ func(x : M 0 ) m : func(x : M 0 ) M D-Sub Γ ⊩ m : M 0 ⊢ M 0 <: M Γ ⊩ m : M D-AbsEmp Γ ⊩ x : M l Γ ⊩ abs K x : M l D-Abs Γ ⊩ (abs K x)(ì p) : func(y : M ′ ) M Γ ⊩ p ′ : M ′ Γ ⊩ (abs K x)(ì p, p ′ ) : M[y → mem Γ (p ′ )] D-Compnt Γ ⊩ m : sig S 1 ; module x : M; S 2 restr θ end Γ ⊩ m.x : M D-FuncApp Γ ⊩ m : func(x : M ′ ) M Γ ⊢ p ′ : M ′ Γ ⊩ m(p ′ ) : M[x → mem Γ (p ′ )]Module structure typing Γ ⊩ θ st : S.D-ProcDecl body = { var ( ì v l : ì τ l ); s; return r } ì v, ì v l fresh in Γ Γ f = Γ, var ì v : ì τ , var ì v l : ì τ l Γ f ⊢ s Γ f ⊢ r : τ r Γ ⊢ body ▷ θ [f ] Γ ⊩ θ st : S Γ ⊩ θ (proc f ( ì v : ì τ ) → τ r = body; st) : (proc f ( ì v : ì τ ) → τ r ; S) D-ModDecl Γ ⊩ m : M Γ ⊩ θ st : S Γ ⊩ θ (module x = m; st) : (module x : M; S) D-StructEmp Γ ⊩ θ ϵ : ϵ Environments typing Γ ⊩ E D-EnvSeq Γ ⊩ Γ 1 Γ ⊩ Γ 2 Γ ⊩ (Γ 1 ; Γ 2 ) D-EnvEmp Γ ⊩ ϵ D-EnvVar Γ(v) = (var v : τ ) Γ ⊩ (var v : τ )

ACKNOWLEDGMENTS

The research leading to these results has received funding the French National Research Agency (ANR) under the project TECAP ANR-17-CE39-0004-01.

This work is financed by National Funds through the FCT -Fundação para a Ciência e a Tecnologia within project PTDC/CCI-INF/31698/2017.

Work by Gilles Barthe was supported by the Office of Naval Research (ONR) under project N00014-15-1-2750. This work received funding from the France 2030 program managed by the French National Research Agency under grant agreement No. ANR-22-PECY-0006.

2 WARM UP EXAMPLE: PKE FROM A ONE-WAY TRAPDOOR PERMUTATION public-key encryption (PKE) scheme proposed by [13] bit-wise xor. We start by a quick presentation of EasyCrypt modules, before delving into the proof of security of this scheme. module BR93 (H : RO) = { proc enc(pk, m) = { var r : rand, h : plaintext; r $ pk r || h ⊕ m); } }.

In the middle code-snippet of Fig. 19 we give an example ideal functionality for a simple one-shot unidirectional authenticated channel; one party provides input with the party identities and the message to transmit (type msg pkg), and the other party can obtain the message if it calls outputs with matching identities (type unit pkg.) The attacker can use the backdoor procedure to observe the state of the channel, including the transmitted message and the party identities and it can use the step procedure to control when the message is delivered (the unlock operator changes the state so that, if a message is buffered, then it is made available at the output procedure) to the receiving party (get_message is checking for identity consistency, which models authentication).

Appendix Outline. We quickly outline the structure of the appendix. We present the remaining typing rules for our programming language and module system in Appendix A. In Appendix B, we give the definition of the additional complexity measures used to define our cost judgements: the ACM Trans. Priv. Sec., Vol. number of calls a program execution makes to some abstract procedure, and the intrinsic cost of a program execution (i.e. the cost of the program without the cost of parameters calls). Appendix C proves that that our type system and module resolution mechanism have the subject reduction property: essentially, evaluating a module expression preserves its type. This is a crucial property, as it proves that module restrictions are preserved by the evaluation of a module using the module resolution mechanism. Finally, we present the full set of rules of our Hoare logic for cost and prove their soundness in Appendix D.

A ADDITIONAL TYPING RULES

To help the reader, we give a summary of all the syntactic categories of our programming language and module system in Fig. 21. The memory restriction union ⊔, intersection ⊓ and the memory restriction subset ⊑ operations are defined in Fig. 22. In Fig. 23, we present our sub-typing rules, our typing rules for statements and expressions, and the definition of the function mem Γ (p) which computes the memory footprint of p in Γ. Note that we need two different rules to type function paths: T-Proc1 does a lookup of the procedure as a component of an already typed module; and T-Proc2 does a lookup of the procedure in the typing environment, in case the procedure is declared in one of the parent modules of the current sub-module being typed (consequently, these modules are not yet fully typed).

A.1 Additional Typing Rules module

Example A.1. Consider the modules and procedures given in Fig. 25. When typing h, the typing environment contains one module declaration and one procedure declaration:

Here, the call to f in h is typed using the T-Proc1 rule, while the call to g is typed using T-Proc2.

B ADDITIONAL INSTRUMENTED SEMANTICS

We give the definition of the additional complexity measures used to define our cost judgements, using two auxiliary instrumented semantics: y.д s E, ρ ν counts the number of times s calls an abstract procedure y.д; and i s E, ρ ν measures the intrinsic cost of an instruction (i.e. without counting the cost of function calls in a functor parameters).

Function call counting. The function call counting semantics y.д s E, ρ ν , given in in Fig. 26, evaluates the instruction s under the memory ν and E-pre-interpretation ρ, counting the number of calls to the abstract procedure y.д.

The maximum number of calls of an instruction s or module procedure m.f to y.д in (E, ρ) is:

#calls Typing Environment:

Module restrictions:

Module signature and structure sub-typing ⊢ M 1 <: M 2 and ⊢ S 1 <: S 2 .

We omit the reflexivity and transitivity rules.

Statements and function paths typing Γ ⊢ s and Γ ⊢ F : _.

T-Abort

Journal pre-print: full version 1:39

Substitution in module signatures and declarations

Substitution in memory restriction

Substitution in module structures, declarations and procedure body And the intrinsic cost in any memory of an instruction s or a module procedure m.f is:

Interpretations. We now define when a pre-interpretation is an interpretation.

C SUBJECT REDUCTION PROPERTY FOR MODULE RESOLUTION

To prove the soundness of our logic, we are going to need to show that our module resolution mechanism has the subject reduction property, i.e. that evaluating a module expression preserves its type. This is a crucial property that allows to show that memory and complexity restrictions are preserved by the evaluation of a module using the module resolution mechanism. That is, the module expression resulting from the evaluation of another module expression has the same memory footprint, and satisfies the same complexity restrictions. Unfortunately, this does not directly hold, for a technical reaspon we describe later (Appendix C.1). We circumvent this problem by defining an alternative notion of typing judgement (Appendix C.2), for which we show that subject reduction does hold (Appendix C.4). This alternative notion of typing judgements for module expressions will be sufficient to prove the soundness of our logic later, in Appendix D.

C.1 Resolution and sub-module declarations

The following example shows why subjet reduction does not hold for our initial notion of typing judgements, because of sub-modules declarations.

Example C.1. Consider a well-typed typing environment ⊢ Γ, and a module path p where:

We are going to assume that some kind of subject reduction property holds for p. More precisely, we assume that:

f-res Γ (p) = (struct st 1 ; module x = m; _ end)

and that we have a derivation:

Γ ⊢ p struct st 1 ; module x = m; _ end : sig S 1 ; module x : M; _ restr _ end Then, we know that p.x resolves to m, i.e. f-res Γ (p) = m. But we do not have:

The problem is that the sub-module m may use sub-modules declared in st 1 . Consequently, it is not well-typed in Γ, but in an extended typing environment, where the sub-module declarations in st 1 (which have types S 1 ) have been added to Γ. For example, we can have:

Therefore, we cannot state a subject reduction property for the module resolution function w.r.t. the typing judgment Γ ⊢ p m : M.

Alternative typing judgements for module expressions. Instead, we introduce another typing judgment, noted Γ ⊩ m : M, which is similar to the typing judgment Γ ⊢ p m : M of Fig. 6, but is used to type a module expression in an environment which has already been typed, while Γ ⊢ p m : M is used to type a module declaration in an environment where some modules have not yet been fully typed. We postpone its definition to Appendix C.2. Using this alternative typing judgment notion, we can state the subject reduction property we want Lemma C.1 (Subject reduction). If Γ ⊩ E and Γ ⊩ m : M then Γ ⊩ res E (m) : M whenever res E (m) is well-defined. Proof outline. The proof is essentially the proof that simply typed λ-calculus has the subject reduction properties, with some consequent additional work to handle module restrictions.

Module expression typing

The rest of this section is organized as follows: we define the typing rules for Γ ⊩ m : M in Appendix C.2, and prove the link between Γ ⊩ m : M and Γ ⊢ p m : M; we present an alternative, more computational, way of defining the module resolution procedure in Appendix C.3; finally, we prove that the module resolution procedure has the subject reduction property in Appendix C.4.

C.2 Typing in Typed Environments

During the resolution of a module expression m, we may have to resolve applied module paths of the form p(p ′ ). This is done by first evaluating p into a functor or an abstract module, and then

Proof. This is by induction over ⊢ Γ. □

We recall that given a module path p, Γ(p) returns the typing declaration corresponding to p in Γ, if it exists. Note that this does not descend in sub-module declarations to retrieve the type of p. For example, assume that: Γ = module p = struct module y = m end : (sig module y : M restr _ end)

then Γ(p) = _:(sig module y:M restr _ end), but Γ(p.y) is not defined. We introduce a new notion of lookup in a typing environment, Γ[p], which descends in sub-module declarations. It also descends below functor definitions, in the case where the functor argument is a module identifier. Continuing the example above, we have Γ[p.y] = m : M. Formally:

Definition C.3. For every well-formed typing environment Γ and module path p, we let:

where the functor rule is module alpha-renaming. Moreover, if: Proof. We show this by induction over the typing derivation Γ, module p : M, Γ 1 ⊩ m : M 0 , by replacing any application of the D-Alias typing rule on a path starting by p, i.e. of the form p(p 0 , . . . , p n ).p ′ , by an application of D-Alias on p, followed by D-Sub and by the applications of D-FuncApp and D-Compnt to replay the path typing derivation of Γ ⊢ p(p 0 , . . . , p n ).p ′ : M as a module expression typing derivation of Γ ⊩ p(p 0 , . . . , p n ).p ′ : M. □ Lemma C.6. For every well-formed typing environment Γ such that Γ(p) undef :

• if Γ ⊢ p m : M then there exists M ′ well-formed in Γ such that ⊢ M ′ <: M and:

n well-formed such that ⊢ D ′ i <:D i for every i, and:

where for every i:

Proof. The proof is by induction over the typing derivations in hypothesis. • the Alias and StructEmp cases are immediate. Note that we use the hypothesis Γ(p) undef in the Alias case, to ensure that the path lookup in Γ is still well-defined. • we show the Struct case by applying the induction hypothesis, and using Proposition C.3.

• for ModDecl we have st = (module x = m 0 ; st 0 ), and S = (module x : M 0 ; S 0 ), and a derivation of the form:

We know that st 0 = (struct d 1 , . . . , d n end) and:

By applying the induction hypothesis twice, we know that there are derivations of: Γ, module p.x = m 0 :

where ⊢ M ′ 0 <: M 0 , and Γ ′′ = (D ′′ 1 , . . . , D ′′ n ) where for every i, ⊢ D ′ i <: D i and:

By Proposition C.4, we deduce from Eq. ( 3) that there is a derivation of: Γ, module p.x = m 0 : M ′ 0 , Γ ′′ ⊩ m 0 : M ′ 0 By Proposition C.5, we deduce from Eq. ( 4) that there is a derivation of: Γ, module p.x = m 0 :

We conclude by applying the D-ModDecl typing rule.

• ProcDecl is similar to the ModDecl case. We omit the details.

• for Sub, we have:

By induction hypothesis, we have a derivation of Γ, module p : M ′ 0 ⊩ m : M ′ 0 where ⊢ M ′ 0 <: M 0 . Using the sub-typing transitivity rule, we have that ⊢ M ′ 0 <: M. This concludes this case.

• for Func we have m = func(x : M 0 ) m ′ and M = func(x : M 0 ) M ′ , and the derivation:

By induction hypothesis, we have M ′′ such that ⊢ M ′′ <: M ′ and:

is derivable. We re-order the declarations in the context, to obtain a derivation of:

(note that the new typing environment is still well-formed). By applying the D-Func rule, there is a derivation of: Γ, module p(x) = m ′ : M ′′ ⊩ func(x : M 0 ) m ′ : func(x : M 0 ) M ′′ By Proposition C.3, there is a derivation of:

We extend sub-typing judgments to typing environments, by requiring that ⊢ Γ 0 <: Γ 1 whenever Γ 0 and Γ 1 are of the same length, and any declaration in Γ 0 is a sub-type of the corresponding declaration in Γ 1 .

Lemma C.7. If ⊢ Γ then there exists ⊢ Γ ′ <: Γ such that Γ ′ ⊩ Γ.

Proof. We use Lemma C.6 to replace the EnvMod rules by D-EnvMod rules. We omit the details. □

C.3 Module Resolution as a Rewrite Relation

We define in Fig. 28 the relation → Γ on partially resolved module expressions. This relation is exactly the evaluation strategy used by the module resolution procedure defined in Fig. 9.

We let m ↓ Γ be the normal form of m w.r. Proof. The fact that → Γ is deterministic is straightforward from the definition of → Γ in Fig. 28: indeed, we only need to observe that well-formed module expressions cannot have two module declarations with the same name.

Moreover, for any m1 and m2 , if m1 → Γ m2 and m1 is well-formed then so is m2 . Hence if → Γ terminates on a well-formed m then m ↓ Γ exists.

Let E be a well-typed environment. We show the second point by induction over the length of the computation of res E ( m). In the environment lookup case, we use the fact that E(p) is either a module structure, functor or an abstract module, and is therefore in → E -normal form. We omit the rest of the proof. □

C.4 Subject Reduction

Before proving that our system has the subject reduction property, we state the following substitution lemmas.

Lemma C.9 (Substitution 1). We have the following substitution properties: • if Γ ⊩ m : M 0 then:

• if Γ ⊢ { var ( ì v l : ì τ l ); s; return e } ▷ λ then:

Proof. We prove the two properties above simultaneously, by induction over the corresponding typing derivations. The proof is straightforward (we omit the details).

Note that we do not need to show closure under substitution of module parameters in Hoare derivations, only in typing derivations (see Remark 3.1).

Proof. W.l.o.g., we assume that the typing derivations Γ ⊩ E and Γ ⊩ m : M never apply the D-Sub typing rules twice in a row (using the transitivity rule for sub-typing judgments). To simplify derivations, we also assume that D-Sub is applied once between each typing rule application (using the sub-typing reflexivity rule if necessary).

We do a case analysis on the reduction m → Γ m ′ . • if x → Γ E(x). We check that we must have a derivation of the following form:

Using the fact that Γ ⊩ E, we know that E = (E 0 ; module x = m : M 0 ; E 1 ) and Γ ⊩ m : M 0 . We conclude by applying D-Sub. • if m.x → Γ m ′ where m = (struct st 1 ; module x = m ′ ; st 2 end). We check that we must have a derivation of the following form:

Hence we have a derivation of Γ ⊩ m ′ : M ′ . We conclude by sub-typing, using the fact that we can derive ⊢ M ′ <: M.

x where m → Γ m ′ , we know that our derivation is of the form: is derivable, we apply Lemma C.12 to get a derivation of:

Using Lemma C.9, we know that since ⊢ M ′′ <: M ′ , we have a derivation of:

• the case where m(p) → Γ (abs K x)(ì p 0 , p) and m = (abs K x)(ì p 0 ) is immediate. □

We recall and prove Lemma C.1:

Lemma (Subject Reduction). If Γ ⊩ E and Γ ⊩ m : M then Γ ⊩ res E (m) : M whenever res E (m) is well-defined.

Proof. From Proposition C.8, we know that res E (m) = m ↓ E . From Lemma C.13, we know that the type of the module expression is preserved. This concludes this proof. □

D SOUNDNESS OF OUR HOARE LOGIC FOR COST

We now prove the soundness of our Hoare logic rules. We recall Theorem 5.1.

Theorem. The proof rules in Figures 12,[START_REF] Barthe | Computer-Aided Security Proofs for the Working Cryptographer[END_REF] and 13 are sound.

We focus on the two most complicated rules of our system, Abs (Section D.1) and Instantiation (Section D.2). The soundness of the remaining rules is straightforward to show (we omit the proof).

First, some notation. We extend the program semantics _