Exequiel Philipp G Haselwarter
email: philipp@haselwarter.org

Antoine Rivas
email: erivas@dcc.fceia.unr.edu.ar

Théo Van Muylder

Carmine Winterhalter
email: theo.winterhalter@mpi-sp.org

Nikolaj Abate

Cătălin Sidorenco
email: sidorenco@cs.au.dk

Kenji Hriţcu

Bas Maillard

Spitters
email: basspitters@cs.au.dk

Exequiel Rivas
email: quielrivas@dcc.fceia.unr.edu.ar

Antoine Van Muylder
email: antoine.vanmuylder@kuleuven.be

Kenji Maillard
email: kenji.maillard@inria.fr

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq

Keywords: CCS Concepts:, Theory of computation → Logic and verification, Programming logic, Categorical semantics, Invariants, Pre-and post-conditions, Program verification, Probabilistic computation, • Security and privacy → Cryptography, Formal methods and theory of security, Logic and verification, high-assurance cryptography, game-based proofs, state-separating proofs, modular proofs, machine-checked proofs, probabilistic relational program logic, formal verification

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

INTRODUCTION

Cryptographic proofs can be challenging to make fully precise and to rigorously check. This has caused a "crisis of rigor" [START_REF] Bellare | The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs[END_REF] in cryptography that Shoup [START_REF] Shoup | Sequences of games: a tool for taming complexity in security proofs[END_REF], Bellare and Rogaway [START_REF] Bellare | The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs[END_REF], Halevi [START_REF] Halevi | A plausible approach to computer-aided cryptographic proofs[END_REF], and others, proposed to address by systematically structuring proofs as sequences of games. This game-based proof methodology is not only ubiquitous in provable cryptography nowadays, but also amenable to full machine-checking in proof assistants such as Coq [START_REF] Barthe | Formal certification of code-based cryptographic proofs[END_REF][START_REF] Petcher | The Foundational Cryptography Framework[END_REF] and Isabelle/HOL [START_REF] Basin | CryptHOL: Game-Based Proofs in Higher-Order Logic[END_REF]. It has also led to the development of specialized proof assistants [START_REF] Barthe | EasyCrypt: A Tutorial[END_REF][START_REF] Blanchet | A Computationally Sound Mechanized Prover for Security Protocols[END_REF] and automated verification tools for cryptographic proofs [START_REF] Barthe | Fully automated analysis of padding-based encryption in the computational model[END_REF][START_REF] Barthe | Automated Proofs of Pairing-Based Cryptography[END_REF][START_REF] Blanchet | A Computationally Sound Mechanized Prover for Security Protocols[END_REF]. There are two key ideas behind these tools: (i) formally representing games and the adversaries against them as code in a probabilistic programming language, and (ii) using program verification techniques to conduct all game transformation steps in a machine-checked manner.

For a long time however, game-based proofs have lacked modularity, which made them hard to scale to large, composed protocols such as TLS [START_REF] Rescorla | The Transport Layer Security (TLS) Protocol Version 1[END_REF] or the upcoming MLS [START_REF] Barnes | The Messaging Layer Security (MLS) Protocol[END_REF]. To address this issue, Brzuska et al. [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF] have recently introduced state-separating proofs (SSP), a methodology for modular game-based proofs, inspired by the paper proofs in the miTLS project [START_REF] Bhargavan | Implementing and Proving the TLS 1.3 Record Layer[END_REF][START_REF] Bhargavan | Proving the TLS Handshake Secure (As It Is)[END_REF][START_REF] Fournet | Modular code-based cryptographic verification[END_REF], by prior compositional cryptography frameworks [START_REF] Canetti | Universally Composable Security[END_REF][START_REF] Maurer | Constructive Cryptography -A New Paradigm for Security Definitions and Proofs[END_REF][START_REF] Maurer | Abstract Cryptography[END_REF], and by process algebras [START_REF] Milner | A Calculus of Mobile Processes[END_REF]. In the SSP methodology, the code of cryptographic games is split into packages, which are modules made up of procedures sharing state. Packages can call each other's procedures (also known as oracles) and can operate on their own state, and adversarial packages in particular cannot directly access other packages' state. Packages have natural notions of sequential and parallel composition that satisfy simple algebraic laws, such as associativity of sequential composition. This law is used to define cryptographic reductions not only in SSP, but also in the The Joy of Cryptography textbook [START_REF] Rosulek | The Joy of Cryptography[END_REF], which teaches cryptographic proofs in a style very similar to SSP.

While the SSP methodology is promising, and has for instance been recently used for proofs of the TLS 1.3 Key Schedule [START_REF] Brzuska | Key-schedule Security for the TLS 1.3 Standard[END_REF] and of the MLS draft standard [START_REF] Brzuska | Security Analysis of the MLS Key Derivation[END_REF], the lack of a complete formalization made SSP only usable for informal paper proofs, not for machine-checked ones. The SSP paper [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF] defines package composition and the syntax of a cryptographic pseudocode language for games and adversaries, but the semantics of this language is not formally defined, and for instance the meaning of their assert operator is neither explained nor self-evident, given the probabilistic setting and the different possible choices, which can affect the meaning of cryptographic security definitions [START_REF] Bellare | Subtleties in the Definition of IND-CCA: When and How Should Challenge Decryption Be Disallowed?[END_REF]. Moreover, while SSP provides a good way to structure proofs at the high-level, using algebraic laws such as associativity, the low-level details of such proofs are usually treated very casually on paper. Yet none of the existing cryptographic verification tools that could help machine-check these low-level details supports the high-level part of SSP proofs: equational reasoning about composed packages (i.e., modules) is either not possible at all [START_REF] Barthe | Formal certification of code-based cryptographic proofs[END_REF][START_REF] Halevi | A plausible approach to computer-aided cryptographic proofs[END_REF][START_REF] Petcher | The Foundational Cryptography Framework[END_REF][START_REF] Swamy | Dependent Types and Multi-Monadic Effects in F*[END_REF], or does not exactly match the SSP package abstraction [START_REF] Barthe | EasyCrypt: A Tutorial[END_REF][START_REF] Lochbihler | Formalizing Constructive Cryptography using CryptHOL[END_REF] (see §8 for a comparison with this related work).

The main contribution of this work is to introduce SSProve, the first general verification framework for machine-checked state-separating proofs. SSProve brings together two different proof styles into a single unified framework: [START_REF] Abate | SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq[END_REF] high-level proofs are modular, done by reasoning equationally about composed packages, as proposed in SSP [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF]; [START_REF] Abel | POPLMark reloaded: Mechanizing proofs by logical relations[END_REF] low-level details are formally proved in a probabilistic relational program logic [START_REF] Barthe | EasyCrypt: A Tutorial[END_REF][START_REF] Barthe | Formal certification of code-based cryptographic proofs[END_REF][START_REF] Petcher | The Foundational Cryptography Framework[END_REF]. Importantly, we show a formal connection between these two proof styles in Theorem 2. [START_REF] Affeldt | Analysis library compatible with Mathematical Components[END_REF].

SSProve is a foundational framework, fully formalized in Coq. To achieve this, we define the syntax of cryptographic pseudocode in terms of a free monad, in which external calls are represented as algebraic operations [START_REF] Plotkin | Algebraic Operations and Generic Effects[END_REF]. This gives us a principled way to define sequential composition of packages based on an algebraic effect handler [START_REF] Plotkin | Handlers of Algebraic Effects[END_REF] and to give machine-checked proofs of the SSP package laws [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF], some of which were treated informally on paper. We formalize the state of SSP packages in terms of a shared global memory and make precise the minimal state-separation requirements, by only requiring disjoint state between adversaries and the games with which they are composed.

Beyond syntax, we also give a denotational semantics to cryptographic code in terms of stateful probabilistic functions that can signal assertion failures by sampling from the empty probability subdistribution. Finally, we prove the soundness of a probabilistic relational program logic for deriving properties about pairs of cryptographic code fragments.

For this soundness proof we build a semantic model based on relational weakest-precondition specifications. Our model is modular with respect to the considered side-effects (currently probabilities, state, and assertion failures). To obtain it, we follow a general recipe by Maillard et al. [START_REF] Maillard | The next 700 relational program logics[END_REF], who recently proposed to characterize such semantic models as relative monad morphisms, mapping two monadic computations to their canonical relational specification. This allows us to first define a relative monad morphism for probabilistic, potentially failing computations and then to extend this to state by applying a relative monad transformer. Working out this instance of Maillard et al.'s [START_REF] Maillard | The next 700 relational program logics[END_REF] recipe involved formalizing various non-standard categorical constructs in Coq, in an order-enriched context: lax functors, lax natural transformations, left relative adjunctions, lax morphisms between such adjunctions, state transformations of such adjunctions, etc. This formalization is of independent interest and could also allow one to more easily add extra side-effects and F ★ -style sub-effecting [START_REF] Swamy | Dependent Types and Multi-Monadic Effects in F*[END_REF] to SSProve in the future.

We formalize several security proofs, starting with the simple illustrative example of PRF-based encryption of Brzuska et al. [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF], followed by a security proof for ElGamal public key encryption inspired by The Joy of Cryptography textbook [START_REF] Rosulek | The Joy of Cryptography[END_REF]Chapter 15.3]. We then put SSProve to the test by formalizing two, more interesting case studies: First, we mechanize the security proof of the KEM-DEM public key encryption scheme of Cramer and Shoup [START_REF] Cramer | Design and Analysis of Practical Public-Key Encryption Schemes Secure against Adaptive Chosen Ciphertext Attack[END_REF], which Brzuska et al. [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF] used to illustrate the main ideas of SSP. The proof extensively uses the package laws of SSP and showcases formal reasoning with invariants. Second, we give a new proof of security of Σ-protocols in SSP style, and show how any Σ-protocol can be used to construct a commitment scheme, which allows us to compare with a similar development in CryptHOL [START_REF] Butler | Formalising 𝛴-Protocols and Commitment Schemes Using CryptHOL[END_REF]. We instantiate the general security proof for Σ-protocols to the concrete example of Schnorr's Σ-protocol [START_REF] Schnorr | Efficient signature generation by smart cards[END_REF] to derive concrete security bounds.

We have already started to reap the benefits of mechanizing SSP in a proof assistant: our mechanization of the KEM-DEM proof of Brzuska et al. [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF] has led us to find-in conjunction with Brzuska et al.-an error in their originally published paper proof. Brzuska et al. have since proposed a revised version of their theorem and proof, which we have adapted and fully mechanized in SSProve. In turn, Markulf Kohlweiss has alerted us about a weakness in the security definition of public-key encryption schemes used in the conference version of the current paper [START_REF] Abate | SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq[END_REF], which we quickly fixed as discussed in §2. [START_REF] Affeldt | Analysis library compatible with Mathematical Components[END_REF]. This demonstrates that the language of SSProve is comprehensible to independent experts, who can review security definitions.

Outline. The remainder of this paper is structured as follows. §2 illustrates the key ideas of how to use SSProve on two simple cryptographic proofs, showing semantic security of PRF-based and ElGamal encryption. In §3 we formalize the SSP methodology: cryptographic pseudocode, packages, sequential and parallel composition, and the algebraic laws they satisfy. In §4 we introduce the rules of a probabilistic relational program logic and use them to prove Theorem 2.4, which formally connects SSP to this program logic. In §5 we outline the effect-modular semantic model we use to prove the soundness of the program logic. In §6 we present a first larger case study, formalizing security of the KEM-DEM public key encryption scheme of Cramer and Shoup [START_REF] Cramer | Design and Analysis of Practical Public-Key Encryption Schemes Secure against Adaptive Chosen Ciphertext Attack[END_REF], following the proof of Brzuska et al. [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF]. In §7 we present the formalization of Σ-protocols in SSProve as a second case study. Remark. A previous version [START_REF] Abate | SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq[END_REF] of the present paper has been published at CSF 2021. The improvements we made throughout the text are too many to list exhaustively. At a high level we: (i) corrected the ElGamal security definition in §2.4; (ii) expanded the explanation of the logical rules in §4 and added new rules for assertions, one-sided memory accesses, and state invariants; (iii) significantly expanded the semantics section to be more self-contained and accessible, and to draw connections to related approaches ( §5); (iv) added Sections 6 and 7 presenting two new case studies; and (v) improved and expanded the related work section ( §8). The paper has also gained a new author, and the author order has also slightly changed.

USING SSPROVE: KEY IDEAS AND EXAMPLES

Formalizing the SSP methodology for high-level proofs allows us to formally link it to the methodology of probabilistic relational program logics for low-level proofs. In this section, we begin with a brief introduction to SSP ( §2.1). Then, we present our new theorem connecting SSP to a probabilistic relational program logic ( §2.2). Finally, by way of two examples, we show how the two methodologies are used together to obtain machine-checked security proofs. The first example looks at a symmetric encryption scheme built out of a pseudo-random function ( §2.3), while the second looks at ElGamal, a popular asymmetric encryption scheme ( §2.4).

An introduction to SSP

We begin by introducing our variant of the SSP methodology of Brzuska et al. [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF]. The main concept behind this methodology is the package, which is a collection of procedure implementations that together manipulate a common piece of state, and that may depend on a set of external procedures. We refer to the set of external procedures on which the package can depend as the imports of the package. In Figure 1, we can see a high-level picture of a package 𝑃: it implements and exports the procedures X and Y, and it imports the external procedure Z. The arrows indicate the direction of calls, i.e., exports that can be called from the outside point towards P and imports point away. We use import(𝑃) to denote the set of procedure names the package 𝑃 imports, and export(𝑃) to denote the names of the procedures it exports. The term interface is used to refer to such a set of procedure names. 1 While the import and export interfaces of a package tell us where it can be used, in the SSP papers, the package implementations are usually given in separate figures, which describe, in pseudocode, each of the procedures exported by the package. For example, a possible pseudocode implementation corresponding to the package 𝑃 can be found in Figure 2. We refer to the code of the procedure X exported by package 𝑃 as 𝑃 .X. In Figure 2, we can also see that the package implementation also depends on some memory location n, which can be read and updated as shown in procedures X and Y respectively. In SSP, such memory cells are implicitly initialized to default values depending on their type; here initially n = 0. In SSProve memory locations refer to a shared global memory and the declaration "mem: n : nat" in package 𝑃 should be understood as: n is the only global memory location that is used by the procedures of 𝑃.

Package algebra. Packages can be combined as algebraic objects. We can build complex packages out of simpler ones using the following composition operations:

• Sequential composition: given two packages 𝑃 1 and 𝑃 2 with import(𝑃 1 ) ⊆ export(𝑃 2 ), then 𝑃 1 • 𝑃 2 is obtained by inlining procedure definitions, each time 𝑃 1 calls a procedure in 𝑃 2 . • Parallel composition: given 𝑃 1 and 𝑃 2 such that export(𝑃 1 ) and export(𝑃 2 ) are disjoint, then 𝑃 1 ∥ 𝑃 2 is the union of 𝑃 1 and 𝑃 2 -it exports the procedures from both 𝑃 1 and 𝑃 2 . • Identity package: given an interface 𝐼 , we have a package that simply forwards all calls in this interface. We refer to it as the identity package on the interface 𝐼 , written ID 𝐼 , and we have that import(ID 𝐼 ) = export(ID 𝐼 ) = 𝐼 . In SSProve sequential and parallel composition are defined even in cases in which the composed packages use the same global memory locations, which allows state sharing.

These operations have graphical counterparts which we show in Figure 3: parallel composition (Figure 3a) is represented by stacking packages on top of each other; sequential composition (Figure 3c) is obtained by merging the input arrows of one of the packages with the output arrows of the other; finally the identity package (Figure 3b) is essentially silent when represented graphically, its presence being notified by longer arrows. Moreover, there are natural algebraic laws that hold between these operators. For example, sequential composition is an associative operator, which formally we can state by the following equation:

𝑃 1 • (𝑃 2 • 𝑃 3 ) code ≡ (𝑃 1 • 𝑃 2 ) • 𝑃 3 (1)
Graphically these laws are obtained by simply forgetting about the dashed boxes (which represent parenthesizing) and by stretching arrows. In the SSP methodology, the code ≡ symbol stands for code equality between the packages: two packages are equal if the implementations of their procedures are equal to each other. As in SSProve code equality corresponds precisely to syntactic equality (including using the same global memory locations), we will write 𝑃 = 𝑄 instead of 𝑃 code ≡ 𝑄 in the remainder of the paper. The aforementioned algebraic package laws (see subsection 3.4 for details) are convenient for cryptographic proofs, since they allow the compositional structure of a package to be manipulated without having to look at all at the implementation of its procedures.

Games and distinguishers.

A package with no imports is called a game. A game pair 𝐺 01 contains two games that export the same procedures, i.e., 𝐺 01 = (𝐺 0 , 𝐺 1 ) such that export(𝐺 0 ) = export(𝐺 1 ) and import(𝐺 𝑏 ) = ∅ for 𝑏 = 0, 1. A distinguisher for a game pair is a package D with import(D) = export(𝐺 0 ) = export(𝐺 1 ) and export(D) = {Run}, where Run is an entry-point procedure that can call the procedures exported by the games and returns a boolean value: true or false. When a game 𝐺 𝑏 exports a single procedure Run : unit → bool as above, we denote by Pr [true ← 𝐺] the probability that 𝐺 .Run returns the boolean value true when running on initial memory. We can quantify how much a distinguisher can distinguish the two packages in a game pair: Definition 2.1 (Distinguisher advantage). The advantage of a distinguisher D against a game pair

𝐺 01 = (𝐺 0 , 𝐺 1 ) is 𝛼 (𝐺 01 ) (D) = Pr true ← D • 𝐺 0 -Pr true ← D • 𝐺 1
Reasoning about advantage. Next, we review the two main results used for equational-like reasoning about advantage against games in SSP: Lemma 2.2 (Triangle Ineqality). Let 𝐺 0 , 𝐺 1 and 𝐺 2 be games, we have that for every distinguisher D,

𝛼 (𝐺 0 , 𝐺 2 ) (D) ≤ 𝛼 (𝐺 0 , 𝐺 1 ) (D) + 𝛼 (𝐺 1 , 𝐺 2 ) (D).
Proof. By unfolding Definition 2.1 we have

𝛼 (𝐺 0 , 𝐺 2 ) (D) = Pr true←D • 𝐺 0 -Pr true←D • 𝐺 2 = |Pr true←D • 𝐺 0 -Pr true←D • 𝐺 1 + Pr true←D • 𝐺 1 -Pr true←D • 𝐺 2 | ≤ Pr true←D • 𝐺 0 -Pr true←D • 𝐺 1 + Pr true←D • 𝐺 1 -Pr true←D • 𝐺 2 = 𝛼 (𝐺 0 , 𝐺 1 ) (D) + 𝛼 (𝐺 1 , 𝐺 2 ) (D)

□

In general, we want to bound the advantage to distinguish 𝐺 0 and 𝐺 𝑛 (i.e., the advantage 𝛼 (𝐺 0 , 𝐺 𝑛 ) (D) against game pair (𝐺 0 , 𝐺 𝑛 )). In order to do so, by repeatedly applying Lemma 2.2, it is enough to exhibit a chain of games 𝐺 0 , 𝐺 1 , 𝐺 2 , . . . , 𝐺 𝑛 so that a bound for 𝛼 (𝐺 0 , 𝐺 𝑛 ) (D) can be given by

𝛼 (𝐺 0 , 𝐺 1 ) (D) + 𝛼 (𝐺 1 , 𝐺 2 ) (D) + . . . + 𝛼 (𝐺 𝑛 -1, 𝐺 𝑛 ) (D).

Lemma 2.3 (Reduction).

Let 𝐺 01 = (𝐺 0 , 𝐺 1 ) be a game pair and let 𝑃 be an arbitrary package. Then, for every distinguisher D, we have

𝛼 (𝑃 • 𝐺 0 , 𝑃 • 𝐺 1 ) (D) = 𝛼 (𝐺 01 ) (D • 𝑃).
Proof. By unfolding Definition 2.1 and applying the associativity law of sequential composition (Equation ( 1)), we have

𝛼 (𝑃 • 𝐺 0 , 𝑃 • 𝐺 1 ) (D) = Pr true ← D • 𝑃 • 𝐺 0 -Pr true ← D • 𝑃 • 𝐺 1 = Pr true ← (D • 𝑃) • 𝐺 0 -Pr true ← (D • 𝑃) • 𝐺 1 = 𝛼 (𝐺 01 ) (D • 𝑃)

□

As its name indicates, Lemma 2.3 is used to reduce the advantage of the distinguisher over a composed game pair (𝑃 • 𝐺 0 , 𝑃 • 𝐺 1 ) to the advantage over part of the game pair 𝐺 01 , for which we know a bound. We will use both these SSP lemmas in §2.3.

Shared state.

As mentioned above, in SSProve we use a shared global memory and composed packages can share state. In particular our sequential and parallel composition are defined even in cases in which the composed packages use the same memory locations. This was easy to formalize in Coq, and allowed us to prove formally that the algebraic laws for package composition as well as the two lemmas above hold even when the involved packages share state.

This treatment of state in SSProve is quite different from the original SSP [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF], in which composed packages have to always be "state separated" (i.e., have disjoint state). To make the state of packages disjoint they allow for 𝛼-renaming of state variables-which shows up for instance in their definition of code equality. Such informal 𝛼-renaming conventions are generally more difficult to formalize in a proof assistant [START_REF] Abel | POPLMark reloaded: Mechanizing proofs by logical relations[END_REF][START_REF] Aydemir | Mechanized Metatheory for the Masses: The PoplMark Challenge[END_REF][START_REF] Urban | Nominal Techniques in Isabelle/HOL[END_REF]. Yet in the absence of 𝛼-renaming, requiring state disjointness everywhere would only increase the proof burden and the clutter in the proved security results (it would require the adversary's state to be disjoint from all intermediate games in the proof).

Adversaries. State separation is, however, still crucial for defining adversaries against game pairs. An adversary A for a game pair is a distinguisher whose memory footprint is disjoint from the footprint of each game in the pair. We define adversaries, the memory footprint of a package, and disjointness of footprints more formally in §3.3.

Perfect game indistinguishability.

We say that the games 𝐺 0 and 𝐺 1 of a game pair 𝐺 01 are perfectly indistinguishable when 𝛼 (𝐺 01 ) (A) = 0 for every adversary A. Perfect indistinguishability is a form of observational equivalence and states that no adversary can learn any information about which game in the pair it is interacting with.

Proving perfect indistinguishability steps in a probabilistic relational program logic

We now present the main novel result brought by SSProve. The SSP laws above deal only with the high-level structure of composed packages. However, we often also need to show that two concrete games are equivalent with respect to what an adversary can learn from using them, i.e., perfect indistinguishability. In SSProve we formally verify this kind of equivalence by reducing it to proving a family of semantic judgments in a probabilistic relational program logic. The logic we use is a variant of pRHL, a probabilistic relational Hoare logic introduced by Barthe et al. [START_REF] Barthe | Formal certification of code-based cryptographic proofs[END_REF] in CertiCrypt. Judgments of this logic are of the form

⊨ { { {(𝑚 0 , 𝑚 1 ). 𝜙} } } 𝑐 0 ∼ 𝑐 1 { { {(𝑚 ′ 0 , 𝑎 0 ), (𝑚 ′ 1 , 𝑎 1 )
. 𝜓} } } and intuitively mean that after separately running the two code fragments 𝑐 0 and 𝑐 1 on the corresponding component of a pair of memories 𝑚 0 , 𝑚 1 satisfying a precondition 𝜙, the final memories 𝑚 ′ 0 , 𝑚 ′ 1 and results 𝑎 0 , 𝑎 1 satisfy the postcondition 𝜓 . When writing pre-and postconditions we write as 𝑝. 𝑀 a function that binds 𝑝 and has body 𝑀 (usually denoted by 𝜆𝑝. 𝑀 in the functional programming community). 2 This notation is handy for writing postconditions, which depend on final memories and on final results.We adopt the convention that the variables 𝑚 0 and 𝑚 1 stand for the state associated to 𝑐 0 and 𝑐 1 in preconditions, the initial memories, and 𝑚 ′ 0 , 𝑚 ′ 1 stand for the corresponding state in postconditions, the final memories. We will omit them from judgments when no ambiguity can arise. We now state the main theorem of SSProve: Theorem 2.4. Let 𝐺 01 = (𝐺 0 , 𝐺 1 ) be a game pair with export interface E = export(𝐺 𝑏 ). Moreover, assume that 𝜓 is a stable invariant that relates the memories of 𝐺 0 and 𝐺 1 , and that it holds on the initial memories.

If for each provided procedure 𝑓 : 𝐴 → 𝐵 ∈ E, we have that for all 𝑎 ∈ 𝐴,

⊨ { { {𝜓} } } 𝐺 0 .𝑓 (𝑎) ∼ 𝐺 1 .𝑓 (𝑎) { { {(𝑚 ′ 0 , 𝑏 0 ), (𝑚 ′ 1 , 𝑏 1 ). 𝑏 0 = 𝑏 1 ∧ 𝜓 (𝑚 ′ 0 , 𝑚 ′ 1 )
} } } then we can conclude that 𝛼 (𝐺 01 ) (A) = 0 for any adversary A.

Intuitively, we ask that both procedures, when run on memories satisfying 𝜓 , yield results drawn from the same distribution and memories still satisfying 𝜓 . We leave the precise definition of stable invariants and how this theorem is proved to §4.2, but the main idea behind this invariant is that it keeps track of a relation between the memories of 𝐺 0 and 𝐺 1 , and that this relation is preserved as different procedures from the interface are called during the execution. This can be understood as a bisimulation argument between packages, where transitions between states come from procedure calls. We illustrate how this theorem is used in the examples from the next two subsections.

Security proof of PRF-based encryption in SSProve

We first illustrate the key ideas of SSProve on a cryptographic proof by Brzuska et al. [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF] that we have verified in Coq using our framework. In this proof, reasoning about composed packages (using Lemmas 2.2 and 2.3 above) allows for a high level of abstraction that drives the proof argument. Some steps of this proof are, however, justified by perfect indistinguishability between games, which involves inspecting the procedures of the games and applying program transformations to show the equivalence. In the previous paper proof [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF] these steps were only justified informally by code inspection. Instead, we have formally verified these steps too, using Theorem 2.4 and our relational program logic.

Brzuska et al. [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF] show how to construct a symmetric encryption scheme out of a pseudo-random function (PRF) and use the SSP methodology to reduce security of the encryption scheme-expressed as IND-CPA-to the security of the pseudo-random function, expressed as being indistinguishable from a package doing random sampling.

The scheme assumes a pseudo-random function called prf with the following signature prf : {0,

1} 𝑛 × {0, 1} 𝑛 → {0, 1} 𝑛
where {0, 1} 𝑛 represents the set of 𝑛-bit sequences. It is possible to formalize and quantify the security of PRF-based encryption as the probability for an adversary to distinguish it from a package that samples from a uniform distribution (real vs random paradigm [START_REF] Rosulek | The Joy of Cryptography[END_REF]). Concretely, given the packages PRF 0 and PRF 1 as in Figure 4, where "<$ uniform S" represents uniform sampling from set S, the advantage of an adversary A against the game PRF 01 = (PRF 0 , PRF 1 ) is defined using Definition 2.1 as follows:

𝛼 (PRF 01 ) (A) = Pr true ← A • PRF 0 -Pr true ← A • PRF 1
The three basic algorithms we use to construct a symmetric encryption scheme out of prf are given in Figure 5. These are not packages themselves, but rather code used inside packages. The security property proposed for this encryption scheme is defined as the advantage on a game pair that captures indistinguishability under chosen-plaintext attack (IND-CPA). We refer to this game pair as IND-CPA 01 , and the packages involved are introduced in Figure 6. Notice that in procedure IND-CPA 1 .Enc the argument msg is never used, the encryption procedure is run on a random msg'. Therefore the advantage of an adversary with respect to the game pair IND-CPA 01 represents the probability that the adversary is able to distinguish the encryption of msg from the encryption of a random bit-string. The security of the encryption procedure with respect to an adversary A against IND-CPA 01 is then 𝛼 (IND-CPA 01 ) (A). ) in terms of (a linear function of) the advantage 𝛼 (PRF 01 ). This technique of game-hops follows the style of inequality reasoning chains from §2.1 (Lemma 2.2), where each step involves establishing the advantage on a game pair, and as a result we obtain a bound on the advantage of the game consisting of the initial and final game.

package: PRF 0 mem: k : option {0, 1} 𝑛 Eval ( x ) : if k = ⊥ then k <$ uniform {0, 1} 𝑛 return prf (k , x) package: PRF 1 mem: T : map [{0, 1} 𝑛 -> {0, 1} 𝑛 ] Eval ( x) : if T [x ] = ⊥ then T[ x] <$ uniform {0, 1} 𝑛 return T[ x]
if k = ⊥ then k <$ uniform {0, 1} 𝑛 (r , c ) ← enc (k , msg ) return (r , c ) package: IND-CPA 1 mem: k : option {0, 1} 𝑛 Enc ( msg ): if k = ⊥ then k <$ uniform {0, 1} 𝑛 msg ' <$ uniform {0, 1} 𝑛 (r ,c) ← enc (k , msg ') return (r ,c)
In this example, IND-CPA 𝑏 is shown equivalent to a variant, MOD-CPA 𝑏 , that gets the pad through the PRF, i.e., with a call to Eval of the package PRF 0 or PRF 1 (see Figure 7). By repeatedly applying Lemma 2.2, we bound 𝛼 (IND-CPA 01 ) (A) by

𝛼 (IND-CPA 0 , MOD-CPA 0 • PRF 0 )(A) + 𝛼 (MOD-CPA 0 • PRF 0 , MOD-CPA 0 • PRF 1 ) (A) + 𝛼 (MOD-CPA 0 • PRF 1 , MOD-CPA 1 • PRF 1 )(A) + 𝛼 (MOD-CPA 1 • PRF 1 , MOD-CPA 1 • PRF 0 )(A) + 𝛼 (MOD-CPA 1 • PRF 0 , IND-CPA 1 )(A)
By observing that 𝛼 (IND-CPA 0 , MOD-CPA 0 •PRF 0 ) (A) = 0, and 𝛼 (MOD-CPA 1 •PRF 0 , IND-CPA 1 )(A) = 0, and by using Lemma 2.3 twice, we reduce this bound to

𝛼 (PRF 01 ) (A • MOD-CPA 0 ) + 𝜀 stat. (A) + 𝛼 (PRF 01 )(A • MOD-CPA 1 ).
where

𝜀 stat. = 𝛼 (MOD-CPA 0 • PRF 1 , MOD-CPA 1 • PRF 1
). The advantage of an attacker with respect to MOD-CPA 0 and MOD-CPA 1 is usually referred to as statistical gap, a polynomial function of the number of calls from the adversary (see [40, appendix A]). One could prove a precise bound based on the birthday paradox here [40, appendix A], but this would require formal reasoning about failure events [START_REF] Barthe | Formal certification of code-based cryptographic proofs[END_REF]. It would be useful to extend SSProve in the future with a unary, union bounds logic for adding more precision to such steps [START_REF] Barthe | A Program Logic for Union Bounds[END_REF].

We can informally interpret the formally proved bound above as saying that if the advantage of A • MOD-CPA 𝑏 against PRF and the statistical gap are negligible then the advantage of A against IND-CPA 01 is also negligible, under the additional assumption that A is probabilistic polynomial time and has disjoint state from PRF 1 , so that A • MOD-CPA 𝑏 is an adversary against PRF 01 . While this disjointness assumption is needed at the top level, when applying Lemma 2.2 for reducing the advantage of the adversary A for game pair IND-CPA 01 , we are basically using A as a distinguisher, which does not introduce additional state disjointness requirements, i.e., for applying Lemma 2.2, the state of A is only required to be disjoint from IND-CPA 01 , not from MOD-CPA 𝑏 and PRF 𝑏 .

It remains to justify the two perfect indistinguishability statements above. These steps involve replacing an informal argument [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF] by a fully formal one, moving to our probabilistic relational program logic. We will detail one of these steps:

𝛼 (IND-CPA 0 , MOD-CPA 0 • PRF 0 ) (A) = 0. The other step, 𝛼 (MOD-CPA 1 • PRF 0 , IND-CPA 1 ) (A) = 0, is analogous.
In order to prove this equivalence, Brzuska et al. [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF] notice that the Enc procedures of IND-CPA 0 and MOD-CPA 0 • PRF 0 (see Figure 8) return the same distributions of ciphertext when called on the same msg. The two procedures are obtained by "inlining" the code of PRF 0 .Eval inside MOD-CPA 0 , and by "unfolding" the code of enc.

IND-CPA 0 .Enc(msg) The left-and right-hand side procedures in Figure 8 only differ when k = ⊥, in which case the left Enc procedure first samples k and then r, while the right Enc first samples r and then k. In both procedures, k and r are drawn from independent distributions. Here Brzuska et al. [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF] conclude informally that independence allows to "swap" the two operations. We instead use Theorem 2.4 to formally reduce 𝛼 (IND-CPA 0 , MOD-CPA 0 • PRF 0 ) (A) = 0 to showing the equivalence of the two Enc procedures from Figure 8. In our probabilistic relational program logic, this comes down to proving the following judgment for all plaintext messages msg,

if k = ⊥ then k <$ uniform {0, 1} 𝑛 r <$ uniform {0, 1} 𝑛 pad ← prf (k , r ) c ← msg xor pad return (r , c ) (MOD-CPA 0 • PRF 0 ).Enc(msg) r <$ uniform {0, 1} 𝑛 if k = ⊥ then k <$ uniform {0, 1} 𝑛 pad ← prf (k ,r) c ← msg xor pad return (r , c)
⊨ { { {(𝑚 0 , 𝑚 1 ). 𝑚 0 = 𝑚 1 } } } IND-CPA 0 .Enc(msg) ∼ (MOD-CPA 0 • PRF 0 ).Enc(msg) { { {(𝑚 ′ 0 , 𝑟𝑐 0 ), (𝑚 ′ 1 , 𝑟𝑐 1 ). 𝑚 ′ 0 = 𝑚 ′ 1 ∧ 𝑟𝑐 0 = 𝑟𝑐 1 } } }
This judgment intuitively states that encrypting msg with the same initial memories "𝑚 0 = 𝑚 1 ", terminates in memories and ciphertexts drawn from the same distribution, "𝑚 ′ 0 = 𝑚 ′ 1 ∧ 𝑟𝑐 0 = 𝑟𝑐 1 ". We use the following instance of the swap rule from §4.1, to formally justify this swapping:3 Fig. 9. Algorithms for ElGamal encryption scheme

⊨ { { {𝑚 0 = 𝑚 1 } } } x <$ uniform {0,1} n ∼ y <$ uniform {0,1} n { { {𝑚 ′ 0 = 𝑚 ′ 1 ∧ 𝑐 0 = 𝑐 1 } } } ⊨ { { {𝑚 0 = 𝑚 1 } } } y <$ uniform {0,1} n ∼ x <$ uniform {0,1} n { { {𝑚 ′ 0 = 𝑚 ′ 1 ∧ 𝑐 0 = 𝑐 1 } } } ⊨ { { {𝑚 0 = 𝑚 1 } } } x <$ uniform {0,1} n ; y <$ uniform {0,1} n ∼ y <$ uniform {0,1} n ; x <$ uniform {0,1} n { { {𝑚 ′ 0 = 𝑚 ′ 1 ∧ 𝑐 0 = 𝑐 1 } } }

Security proof of ElGamal in SSProve

We also illustrate the key ideas of SSProve on a security proof for the ElGamal encryption scheme inspired by The Joy of Cryptography textbook [START_REF] Rosulek | The Joy of Cryptography[END_REF]Chapter 15.3]. ElGamal belongs to the family of public-key or asymmetric encryption schemes, which use a public key for encryption and a private key for decryption. Public-key schemes therefore require a key generation algorithm producing the pair of public and private keys. In our formalization it suffices to provide the aforementioned algorithms together with key-, plaintext-and cipher-spaces to automatically obtain a public-key scheme together with its related security notions (to be proved) such as security against chosen plaintext attacks (CPA). In what follows we describe which spaces and algorithms define ElGamal and the security proof we provided for it.

ElGamal is parameterized by a multiplicative cyclic group (G, *) with 𝑛 elements and with generator 𝑔, usually denoted by ⟨𝑔⟩ = G. Plaintexts are elements 𝑚𝑠𝑔 ∈ G and ciphertexts are pairs of group elements 𝑐 = (𝑐 rnd , 𝑐 msg ) ∈ G × G. Secret keys are elements of Z 𝑛 , while public keys are group elements once again, pk ∈ G. The key generation algorithm (KeyGen in Figure 9) generates a secret key that is a random number sk ∈ {0, . . . , 𝑛 -1} and a public key that is 𝑔 sk . Encryption and decryption (Enc and Dec in Figure 9) involve the group operation (_*_), exponentiation (_) _ and the multiplicative inverse (_) -1 . Encryption works probabilistically, generating an ephemeral key rnd to derive a shared secret shs which is used to encrypt the plaintext message msg.

Under the Decisional Diffie-Hellman (DDH) assumption for the group G, namely that DDH 0 and DDH 1 from Figure 10 are computationally indistinguishable, one can prove that an adversary cannot distinguish messages encrypted with the ElGamal scheme from ciphertexts that are randomly sampled (CPA). Our formalization only considers the case in which the adversary can see a single ciphertext (one-time CPA, written OT-CPA), as it is known that this suffices for public-key encryption schemes to satisfy CPA [START_REF] Rosulek | The Joy of Cryptography[END_REF]Claim 15.5]. We leave the formalization of this last result as future work and discuss hereafter our proof of OT-CPA in SSProve.

The security property OT-CPA is expressed in terms of the advantage against game pair CPA 01 in Figure 11. An adversary A can call Get_pk() and get the public key, if already initialized. 4 The adversary can "challenge" a package to encrypt a certain plaintext msg through Challenge(msg). Both packages return a ciphertext only if the counter is 0-as expressed by the use of assert-so the adversary can only see one ciphertext. Both packages call KeyGen to generate public and private keys, but while CPA 0 indeed encrypts the message provided by the adversary with the public key through Enc(pk, msg), the package CPA 1 instead returns a randomly sampled ciphertext was not a proper public-key scheme. We thank Markulf Kohlweiss for making us aware of this flaw, which was easy to fix. Formalizing the connection between OT-CPA and CPA [START_REF] Rosulek | The Joy of Cryptography[END_REF]Claim 15.5] (c rnd , c msg ) <$ uniform G × G, i.e., a pair of group elements sampled from the uniform distribution on G × G.

The OT-CPA proof reduces the advantage of adversary A against (CPA 0 , CPA 1 ) to the advantage of A • MOD-CPA against (DDH 0 , DDH 1 ), with the auxiliary package MOD-CPA listed in Figure 12:

𝛼 (CPA 01 ) (A) ≤ 𝛼 (DDH 01 ) (A • MOD-CPA).
We once again obtain this result by repeatedly applying Lemma 2.2 to bound 𝛼 (CPA 01 ) (A) by

𝛼 (CPA 0 , MOD-CPA • DDH 0 ) (A) + 𝛼 (MOD-CPA • DDH 0 , MOD-CPA • DDH 1 ) (A) + 𝛼 (MOD-CPA • DDH 1 , CPA 1 ) (A)
We prove that the first and last advantages are null by proving the packages perfectly indistinguishable, and the remaining advantage is equal to 𝛼 (DDH 01 ) ( Step 𝛼 (CPA 0 , MOD-CPA • DDH 0 ) (A) = 0: We apply Theorem 2.4 and reduce the goal to a relational judgment between CPA 0 .Challenge(msg) and (MOD-CPA • DDH 0 ).Challenge(msg) for a generic plaintext msg, and where the invariant 𝜓 is equality of memories. Inlining the code of Query provided by DDH 0 inside MOD-CPA and unfolding one realizes that the two code fragments are identical and the judgment holds by application of the reflexivity rule in §4.1.

Step 𝛼 (MOD-CPA • DDH 1 , CPA 1 ) (A) = 0: This step is quite similar to the one above. After inlining, however, the two code fragments are not exactly the same, since in particular CPA 1 completely ignores msg and returns a random ciphertext, while MOD-CPA • DDH 1 returns msg*g rnd' for a random rnd'. To have equality of memories as invariant 𝜓 , we show that in G, multiplication by g^(_) acts like a one time pad, which is a standard result [26, Section 6.2].

FORMALIZING STATE-SEPARATING PROOFS

We separate the programming language and thus the reasoning into two strata: code and packages. We define the syntax of code ( §3.1), relate it to the notation used in §2.1, and explain its semantics ( §3.2). We then give a formal description of packages ( §3.3) and the algebraic laws they obey ( §3.4). In §2.1 we took some license regarding notation in order to stay close to the presentation of Brzuska et al. [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF]. The code examples in the remainder of the paper more faithfully follow the Coq notations we use in the formal development of SSProve.

Syntax for cryptographic code (free monad)

The language of the Coq system, Gallina, is a dependently typed, purely functional programming language. As such, we can directly express functional code in Gallina, but not code with side-effects such as reading from and writing to memory, probabilistic sampling, or external procedure calls. We thus represent cryptographic code via a combination of the ambient language Gallina and a monad of effectful computations. Monads constitute an established way of adding effects to a purely functional language [START_REF] Moggi | Computational Lambda-Calculus and Monads[END_REF][START_REF] Wadler | Comprehending Monads[END_REF]. Free monads in particular allow to separate the representation (syntax) of an embedded language from its interpretation (semantics).

Raw code. We use a hybrid approach [START_REF] Petcher | The Foundational Cryptography Framework[END_REF] of embedding the pure fragment of our cryptographic programming language shallowly in Coq, and embedding the effects deeply via a free monad. This free monad is defined as an inductive type:5

Inductive raw_code A :

Type : = | return ( x : A ) | call ( p : opsig ) ( x : src p ) ( 𝜅 : tgt p → raw_code A ) | get ( ℓ : Location ) ( 𝜅 : type ℓ → raw_code A ) | put ( ℓ : Location ) ( v : type ℓ ) ( 𝜅 : raw_code A ) | sample ( op : Op ) ( 𝜅 : dom op → raw_code A ) .
Some more explanations about raw_code are in order. The type parameter A indicates the result of a computation of type raw_code A. The first clause of the above definition lets us inject any pure value x of type A into the monad as return x. Calls to external procedures are represented via call p x 𝜅, where the first argument p : opsig specifies the name of the procedure, the type of its argument (src p), and its return type (tgt p). The second argument x is the input value of type src p passed to the called procedure. The last argument 𝜅 is the continuation of the program, awaiting the result of the call to p. The get and put operations take a (typed) global memory location ℓ as argument, respectively read from and write to that location, and continue with the continuation 𝜅. Finally, we may sample from a collection of probabilistic subdistributions Op. Subdistributions constitute the base of our code semantics and are further discussed in §3.2. The type Op is a parameter of the language that can be instantiated by the user. Sampling a subdistribution op on type dom op (the domain of the subdistribution) can be composed with a matching continuation 𝜅 (continuations are explained below).

We will use the following two pieces of code as running examples to explain different aspects of the definition.

get ℓ (λ x ℓ . put ℓ (x ℓ + 1) (return x ℓ )) (2) sample (uniform {0, 1} 𝑛 ) (λ y . call Prf (y, 101010) (λ z . return z)) (3)
The code in (2) increments the value stored at location ℓ by 1 and returns the value before the increment. The code in (3) draws a random bit-string y of length 𝑛, calls an external procedure Prf with arguments y and bit-string 101010, and returns the result.

Code with locations and interface. Raw code is merely a representation of syntax. To record which imported procedures and global memory locations are used, we introduce a corresponding predicate. We consider the code with respect to set of locations L and to an import interface I which is a set of procedure signatures (opsig) consisting of a name, an input type and an output type. The predicate checks that all reads and writes performed in the code are made to locations in L and that all imported procedures belong to I. Concretely, the code in (2) uses locations in the singleton set {ℓ} and has the empty import interface, while (3) uses the empty set of locations and the interface {Prf : {0, 1} 𝑛 × {0, 1} 𝑛 → {0, 1} 𝑛 }. The type code L,𝐼 is then simply defined as raw code that verifies the predicate corresponding to locations L and import interface I:

code L,𝐼 A = { c : raw_code A | has_locs_and_imports c L I }
In the paper we sometimes omit the set of locations and the interface. Thanks to the use of tactics and Coq's type classes, proofs regarding these locations and interfaces for well-scoped user-written code are constructed automatically without requiring user intervention.

Locations are typed, which means that each ℓ in L is designated a specific type that corresponds to the type of data stored in the respective memory cell. The type assigned to ℓ is denoted by type ℓ.

Continuations. A continuation is a suspended computation awaiting the result of an operation, intuitively corresponding to the rest of the program. Consider for instance the code (2). The get operation performs a memory lookup at the location ℓ, and its continuation is a Coq function "(λ x ℓ . put ...) " of type "type ℓ → raw_code nat" that receives the value stored at ℓ as its parameter 𝑥 ℓ . The continuation in turn performs a put operation, storing the value 𝑥 ℓ + 1 at memory location ℓ, and returns the value 𝑥 ℓ . The code thus corresponds to the expression written as ℓ++ in common imperative languages.

Variables. As demonstrated in example (2), we draw a strict distinction between a location ℓ, which can be accessed and updated via get and put, and the value stored in memory at location ℓ. In (2), this value is available in the continuation of get ℓ (λx ℓ . put ...) as x ℓ . Formally speaking, x ℓ is an immutable Coq variable, and in (2) the location ℓ itself is a Coq variable of type Location. This distinction is already present in SSP [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF]Def. 2], where locations correspond to "state variables" and the ambient, mathematical notion of variable is referred to as "local variable".

Memory initialization.

As mentioned in §2.1, memory locations are implicitly initialized to default values depending on their type (for instance in Figure 2 n is initialized to 0). Yet we frequently want to clearly distinguish the case when a location was implicitly initialized to a default value from the case when it was explicitly initialized. For instance, in Figure 6 we want to distinguish the case in which the key k has not yet been generated from the case in which it has been. To achieve this we define the type of the k as option key, using the following standard definition for the option type:

Inductive option A : = ⊥ | Some ( a : A ) .
Memory locations of type option key are implicitly initialized to the dummy value ⊥, which is different from any generated key, which is tagged with the constructor Some.

Monadic bind. The bind operation of the monad, with type code A → (A → code B) → code B, allows the composition of effectful code. Take for instance the following pieces of code.

Definition c : code nat : = sample ( uniform bool ) ( λb . if b then return m 1 else return m 2 ) Definition 𝜅 : nat → code nat : = λm . put ℓ m ( return 0 )
We would like to use c as an argument to 𝜅, but the types don't match: 𝜅 expects a value of type nat as argument, not a computation of type code nat. We define a standard bind operation that achieves this by traversing the code of c, applying 𝜅 when a returned value is encountered, and recursively pushing 𝜅 into any other continuations.

Fixpoint bind ( c : code A ) ( 𝜅 : A → code B ) : code B : = match c with | return a ⇒ 𝜅 a | call p v 𝜅 ' ⇒ call p v ( λ x . bind ( 𝜅 ' x ) 𝜅 ) | get l 𝜅 ' ⇒ get l ( λ v . bind ( 𝜅 ' v ) 𝜅 ) | put l v 𝜅 ' ⇒ put l v ( bind 𝜅 ' 𝜅 ) | sample op 𝜅 ' ⇒ sample op ( λ a . bind ( 𝜅 ' a ) 𝜅 ) end
An easy structural induction over code allows us to prove that bind satisfies the expected monad laws: bind is associative (bind m (λ p . bind (f p) g) = bind (bind m f) g), and return serves as a unit (bind (return x) f = f x and bind m return = m).

Loops. We do not have syntax for loops in code. However, since we are embedding in Coq we take advantage of its recursion mechanisms to write terminating loops. The most basic construction we can write is a "for i := 0 to N do c" loop that repeats (N+1)-times a command c, providing to c the value of the index i. In the code below, the pattern matching happens over the natural number N, which in Coq is represented in unary format, so it is either 0 (zero) or S n (read successor of n, for some natural number n).

Fixpoint for_loop ( N : nat ) ( c : nat → code unit ) : code unit : = match N with | 0 ⇒ c 0 | S n ⇒ bind ( for_loop n c ) ( λ _ . c N ) end .
More generally, we can define a "do-while" loop that repeatedly executes a loop body while a condition holds, checked after each iteration. To ensure termination in Coq we add a natural number N to bound the maximum number of iterations:

Fixpoint do_while ( N : nat ) ( c : code bool ) : code bool : = match N with | 0 ⇒ return false | S n ⇒ bind c ( λb . if b then do_while n c else return true ) end .
At the end, the returned boolean signals whether there was remaining fuel (i.e., iteration steps) available or not. In the future, we hope to extend SSProve to potentially non-terminating loops, since the semantic models of probabilistic programs usually support general fixpoints (as further discussed in §5.5).

Standard subdistributions. Probabilistic operations denoting a collection of subdistributions we may sample from are included in the type Op, which is a parameter of our language. Standard subdistributions including uniform sampling on finite types as well as a null subdistribution are predefined for convenience. The null subdistribution in particular allows us to represent failure and an assert construct. Failure at type A is defined as sampling from the null distribution dnull.

Definition fail A : code

A : = x ← sample dnull ; return x .
A simple assertion is not expected to produce any interesting values but only gets evaluated for the possibility of failing if the condition is violated. This is expressed by the fact that a successful assert simply returns a value of unit type, where unit is Coq's singleton type with a unique inhabitant () .

Definition assert ( b : bool ) : code unit : = if b then return ( ) else fail unit .

If b is true, then assert returns the trivial value () , but if b is false, we instead sample from the dnull subdistribution via fail unit, assigning probability zero to all values of the type unit (i.e., to () ). Sampling from the null subdistribution is similar to non-termination, and means that the continuation will never be called. This provides a simple and clearly defined semantics for assertion failures. While this is not the only choice [START_REF] Bellare | Subtleties in the Definition of IND-CCA: When and How Should Challenge Decryption Be Disallowed?[END_REF][START_REF] Dupressoir | Bringing State-Separating Proofs to EasyCrypt -A Security Proof for Cryptobox[END_REF][START_REF] Rogaway | Simplifying Game-Based Definitions -Indistinguishability up to Correctness and Its Application to Stateful AE[END_REF], this formalizes our understanding of the following informal convention from the paper introducing SSP [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF]: "all our definitions and theorems apply only to code that never violates assertions. "

We can see this use of assert in Figure 11 from §2.4. The packages CPA 𝑏 ensure that the Challenge procedure can be called only once by running assert counter = 0. If the assertion succeeds, we may assume that counter = 0 holds in the rest of the procedure, until counter is incremented. We can demonstrate how distinguishers interact with procedures calling assert by computing Pr true ← D • CPA 𝑏 (as used in Definition 2.1) for a distinguisher D that calls Challenge twice on some fixed message before always returning true. Even though the distinguisher still returns true in this scenario, assert will fail the second time the distinguisher calls Challenge, and thus the subdistribution represented by D • CPA 𝑏 .Run becomes the null subdistribution. It follows that Pr true ← D • CPA 𝑏 = 0.

The simple use of assert above is "logical": we limit the input to certain functions or the ways in which protocols can be called in order to exploit these assertions in our security reasoning. A more complex use of assertions, which we call "dependent", occurs in the following example. Consider the situation where we have a memory location ℓ : Location holding a key which is initialized to ⊥. Formally, this amounts to the information type ℓ = option key, which may be presented in the signature of a package as mem: ℓ : option key. We did not distinguish immutable variables and locations in §2, but we carry out a careful analysis of memory initialization in the KEM-DEM case study in §6. For instance, we will see in Figure 14 ( §6, Page 36) an implementation of a Get() procedure that returns the key stored at location k_loc. This procedure defines a partial function of type unit → key, that fails to return a value if the memory location has not yet been explicitly initialized (i.e., it is ⊥). We first retrieve the potentially not explicitly initialized key from memory as k, of type option key.

We then check via a dependent assert that k is not ⊥, and record the asserted condition as kSome of type k ≠ ⊥. We can now apply getSome with kSome to safely coerce k from option key to key. In this example, the code that follows the assertion depends on the asserted condition, whereas in the previous example with counter the assertion was only used when reasoning in the relational program logic. Indeed the continuation of dependent assert, called kont in the declaration below, has type b = true → code A. In other words, it constitutes a piece of code, computing a value of type A, that is defined only when the assertion b is true. Operationally assertD is similar to the simple assert above, but the actual Coq definition in terms of fail and a conditional is more complicated because it uses dependent elimination to type-check the success branch. Since such details are not important here, we refer the interested reader to the Coq source and only show the type of this operator:

Definition assertD A b ( kont : b = true → code A ) : code A .
Procedure calls. A call to an external procedure such as Prf in (3) is represented by the call operation, taking as arguments a procedure name p annotated with a type, a value matching the argument type of p, and a continuation 𝜅 matching the return type of p. In §3.3 we show how an implementation gets substituted for this placeholder via sequential package composition.

Notation. The use of continuations is pervasive in monadic code, and to alleviate the presentation we introduce the following more familiar notation. In code listings we will frequently omit the ; separator when it would occur at the end of a line. We will also write c 1 ; c 2 for _ ← c 1 ; c 2 when the continuation c 2 does not use its argument.

Correct typing. The typing constraints imposed by the raw_code definition enforce correct typing for user-written code, guaranteeing that operations and their continuations are compatible. For instance, let the continuation of get in (2) be f. Then f is only compatible with ℓ if f's domain matches the type of ℓ, i.e., f : type ℓ → raw_code A for some type A.

Syntax at work. We now illustrate our formal syntax in action. For this we restate the procedure PRF 0 .Eval(x) from Figure 4 more formally using raw_code and the various notations above:

Definition Eval ( x : {0, 1} 𝑛 ) : raw_code {0, 1} 𝑛 : = val_k_opt ← get k ; if val_k_opt = ⊥ then y <$ uniform {0, 1} 𝑛 ;
put k : = Some y else return ( ) ; assert ( k ≠ ⊥) as kSome ; let val_k : = getSome k kSome in return prf ( val_k , x ) .

Here we mix constructors of raw_code with other Gallina terms such as the match construct. The result of the match is made available to the continuation of the code as val_k via a use of bind (under the guise of 'val_k ← ... ; ... ').

Semantics of cryptographic code

When no external procedure calls (call o x k) appear in a piece of code c : code A, it is possible to interpret c as a state-transforming probability subdistribution of type

Pr_code c : mem → SD ( A × mem )
This semantics is similar to that of CertiCrypt [START_REF] Barthe | Formal certification of code-based cryptographic proofs[END_REF]. The type SD A denotes the collection of all subdistributions over type A. Generally speaking, a subdistribution is a function 𝑑 : 𝐴 → R assigning a certain probability 𝑑 (𝑎) to each 𝑎 : 𝐴 in such a way that ∫ 𝐴 𝑑 ≤ 1. We use the definition of subdistributions from mathcomp-analysis [START_REF] Affeldt | Analysis library compatible with Mathematical Components[END_REF][START_REF] Mahboubi | Mathematical components[END_REF], a Coq library from which we use the foundations it gives to discrete probability theory. The semantics function Pr_code is defined by recursion on the structure of c. Its definition basically boils down to providing an effect handler that interprets state and probabilities in the monad mem → SD(-× mem).

Using this subdistribution semantics, we can formalize the notation Pr[𝑏 ← 𝐺] from §2.1 as follows: (i) extract the Run function from 𝐺; (ii) apply Pr_code to it; (iii) run it on the initial memory; (iv) extract the boolean component (first projection) from the resulting subdistribution. The final result has type d : SD bool, the type of subdistributions for booleans, and we precisely define Pr[𝑏 ← 𝐺] = d(𝑏) as the probability assigned to 𝑏 by this subdistribution on booleans. A raw package is a finite map from names to raw procedures, which are functions from some A to raw_code B. An interface is a finite set of operation signatures (opsig), each specifying the name, argument type, and result type of a procedure. A package is then a raw package RP together with an import interface I, an export interface E, and a set of locations L, such that each procedure in RP uses only locations in L and imports only from I, and each procedure name listed in E is implemented by a procedure in RP of the appropriate type. Consider for instance the package MOD-CPA in Figure 13. The memory used, mem(MOD-CPA), 6 consists of two locations, pk : option pubKey and counter : nat. The import interface import(MOD-CPA) contains a single procedure Query : unit → G × G × G. There are two procedures implemented by MOD-CPA, yielding an export interface export(MOD-CPA) containing Get_pk : unit → option pubKey and Challenge : G → option (G × G).

We define composition of packages, following the intuition of Brzuska et al. [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF]. Given two raw packages 𝑃 and 𝑄 we define their sequential composition 𝑄 • 𝑃 by traversing 𝑄 and replacing each call by the corresponding procedure implementation in 𝑃. In case 𝑃 does not implement the procedure for which we search, we use a dummy value instead. If the exports of 𝑃 match the imports of 𝑄-i.e., import(𝑄) ⊆ export(𝑃)-then no dummy value will be used. Concretely, during the traversal each call p a 𝜅 node is replaced by

bind ( P . p a ) ( λ x . link 𝑃 ( 𝜅 x ) )
where link 𝑃 stands for the recursive call of the function composing 𝑃 with the remaining code. Experts will recognize this transformation as an algebraic effect handler [START_REF] Bauer | Programming with algebraic effects and handlers[END_REF], interpreting the free monad for probabilities, state and the operations imported by 𝑃 to code in the free monad for probabilities, state, and the operations imported by 𝑄. We have mem(𝑄

• 𝑃) = mem(𝑃) ∪ mem(𝑄), import(𝑄 • 𝑃) = import(𝑃) and export(𝑄 • 𝑃) = export(𝑄).
Given two raw packages 𝑃 and 𝑄 we may define their parallel composition 𝑃 ∥ 𝑄 by aggregating the implementations and delegating calls to the respective package providing it. This operation is defined even if both packages have overlapping export signatures, in which case procedures in 𝑃 will be given priority. If their exports are disjoint, i.e., export(𝑃) ∩ export(𝑄) = ∅, then this overlap situation does not happen and we have mem(𝑃 ∥ 𝑄) = mem(𝑃) ∪ mem(𝑄), import(𝑃 ∥ 𝑄) = import(𝑃) ∪ import(𝑄) and export(𝑃 ∥ 𝑄) = export(𝑃) ∪ export(𝑄).

Private state. When formalizing composition in SSProve we do not impose any a priori restrictions on the disjointness of the state that the composed packages manipulate. The essence of state separation can be thus viewed as disjointness of state between the adversary A and the games in a pair 𝐺 01 . We therefore introduce the more economical assumption that only the adversary has to have disjoint state in our security definitions and corresponding theorem statements (e.g., Theorem 2.4). Formally, an adversary A to game pair 𝐺 01 is thus a distinguisher for 𝐺 01 with the additional assumption that mem(A) is disjoint from both mem(𝐺 0 ) and mem(𝐺 1 ). This extra state assumption sets apart adversaries from distinguishers: we do not require that the state of a distinguisher be disjoint from the game pair it tries to distinguish, and we still proved Lemma 2.2 and Lemma 2.3 from §2.1. The difference between distinguishers and adversaries manifests, for instance, in the definition of perfect indistinguishability from the end of §2.1, which quantifies only over adversaries. Distinguishers that are not adversaries could otherwise directly access the game state and trivially distinguish the games we want to consider indistinguishable.

In the setting of SSProve, in which memory locations are global and not up to 𝛼-renaming, this fine-grained state separation is helpful, since not only it minimizes the burden of formally proving disjointness, but it also reduces the clutter in the statement of the final results.

Automation of side conditions. In our Coq formalization, we provide automation for the checking of side conditions required to build packages and their compositions. This includes checking predicates such as has_locs_and_imports to ensure that the implementation of a package is consistent with the expected interface and memory footprint. There are limitations, however, to the scope of the automation; specifically checking disjointness of location sets is currently quite basic. We plan to improve this situation in future work.

Package laws

We formally proved the algebraic laws obeyed by packages as stipulated by Brzuska et al. [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF]. Sequential composition is associative and parallel composition is commutative and associative, so for any packages 𝑃 1 , 𝑃 2 , 𝑃 3 :

𝑃 1 • (𝑃 2 • 𝑃 3 ) = (𝑃 1 • 𝑃 2 ) • 𝑃 3 𝑃 1 ∥ 𝑃 2 = 𝑃 2 ∥ 𝑃 1 𝑃 1 ∥ (𝑃 2 ∥ 𝑃 3 ) = (𝑃 1 ∥ 𝑃 2 ) ∥ 𝑃 3 .
We furthermore relate the two package operations with an interchange law stating that

(𝑃 1 • 𝑃 3 ) ∥ (𝑃 2 • 𝑃 4 ) = (𝑃 1 ∥ 𝑃 2 ) • (𝑃 3 ∥ 𝑃 4 ).
Commutativity of parallel composition only holds if the packages have indeed disjoint interfaces: export(𝑃 1 ) ∩ export(𝑃 2 ) = ∅. The interchange law will only ask this of 𝑃 3 and 𝑃 4 : export(𝑃 3 ) ∩ export(𝑃 4 ) = ∅.

The identity package ID 𝐼 behaves as an identity for sequential composition when using the correct interface:

ID export(𝑃 ) • 𝑃 = 𝑃 = 𝑃 • ID import(𝑃 ) .
As we have hinted before, these laws do not require disjointness of state, because they are syntactic equalities. In fact, in SSProve they hold with respect to the usual equality of Coq ("propositional equality", written _ = _), without the need to define a separate notion of "code equality" [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF].

PROBABILISTIC RELATIONAL PROGRAM LOGIC

Some of the SSP proof steps can be carried out at a high-level of abstraction relying on the package formalism from §3. The justification of other steps like perfect indistinguishability requires, however, a finer, lower-level analysis. As already pointed out in §2.2, we can perform such analyses in a relational program logic, a deductive system in which it is possible to show that two pieces of code 𝑐 0 , 𝑐 1 satisfy a certain relational specification, e.g. that they are equivalent.

In §4.1 we present some of the elementary rules constituting our program logic. We then sketch a proof of Theorem 2.4, the link between the high-level reasoning based on the package laws to the low-level one based on our probabilistic relational program logic in §4.2.

Selected rules

The logic we use is a variant of pRHL, a probabilistic relational Hoare logic introduced by Barthe et al. [START_REF] Barthe | Formal certification of code-based cryptographic proofs[END_REF]. The logic exposes relational judgments of the form

⊨ { { {(𝑚 0 , 𝑚 1 ). 𝜙} } } 𝑐 0 ∼ 𝑐 1 { { {(𝑚 ′ 0 , 𝑎 0 ), (𝑚 ′ 1 , 𝑎 1 ). 𝜓} } },
for which a basic intuition is provided in §2.2. Formally, 𝑐 0 and 𝑐 1 denote probabilistic stateful code with return type 𝐴 0 and 𝐴 1 respectively, and the precondition 𝑚 0 : mem, 𝑚 1 : mem ⊢ 𝜙 : P is a proposition with free variables 𝑚 0 and 𝑚 1 denoting the initial state of the memory (before execution of the code). The postcondition 𝑚 ′ 0 : mem, 𝑎 0 : 𝐴 0 , 𝑚 ′ 1 : mem, 𝑎 1 : 𝐴 1 ⊢ 𝜓 : P is a predicate on the values returned by the executed code, which is parameterized by the variables 𝑚 ′ 0 and 𝑚 ′ 1 representing the final state of the memory (after execution) and by the final values 𝑎 0 and 𝑎 1 . As mentioned before, we will sometimes omit the quantifications when they are clear from the context. We will also abuse notation and sometimes write e.g., 𝜓 (𝑚 ′ 0 , 𝑎 0 ) (𝑚 ′ 1 , 𝑎 1 ) for the substitution of 𝜓 with the given memories and values. The code fragments appearing in a judgment are drawn from the free monad code L,𝐼 of §3.1, and meet the further requirement that no oracle calls call o x k appear in them (exactly as in §3.2). The precondition 𝜙 is defined to be a relation between initial memories (for instance, 𝑚 0 = 𝑚 1 ). Similarly the postcondition 𝜓 relates final memories and final results, intuitively obtained after the execution of 𝑐 𝑖 on 𝑚 𝑖 . We describe how to assign a formal semantics for such probabilistic judgments in §5.2. The semantics is based on the notion of probabilistic couplings, already adopted by Barthe et al. [START_REF] Barthe | Relational Reasoning via Probabilistic Coupling[END_REF]. In the remainder of this subsection we describe a selection of our rules. The presentation does not contain all the rules employed in practice by SSProve, nor does it provide a canonical presentation of these rules: some rules are overlapping hence there are multiple ways to prove the same relational judgment, but the actual derivation might be simpler with this redundancy. We return to the question of the organization of rules after this presentation.

𝑐 : code L 𝐴 ⊨ { { {𝑚 0 = 𝑚 1 } } } 𝑐 ∼ 𝑐 { { {(𝑚 ′ 0 , 𝑎 0 ), (𝑚 ′ 1 , 𝑎 1 ). 𝑚 ′ 0 = 𝑚 ′ 1 ∧ 𝑎 0 = 𝑎 1 } } } reflexivity
The reflexivity rule relates the code 𝑐 to itself when both copies are executed on identical initial memories.

𝑐 0 : code L 0 𝐴 0 𝑐 1 : code L 1 𝐴 1 𝜅 0 : 𝐴 0 → code L 0 𝐵 0 𝜅 1 : 𝐴 1 → code L 1 𝐵 1 ⊨ { { {𝜙} } } 𝑐 0 ∼ 𝑐 1 { { {𝜒} } } ∀𝑎 0 𝑎 1 . ⊨ { { {(𝑚 0 , 𝑚 1 ). 𝜒 (𝑚 0 , 𝑎 0 ) (𝑚 1 , 𝑎 1 )} } } 𝜅 0 (𝑎 0 ) ∼ 𝜅 1 (𝑎 1 ) { { {𝜓} } } ⊨ { { {𝜙} } } 𝑎 0 ← 𝑐 0 ; 𝜅 0 (𝑎 0 ) ∼ 𝑎 1 ← 𝑐 1 ; 𝜅 1 (𝑎 1 ) { { {𝜓} } } seq
The seq rule relates two sequentially composed commands using bind by relating each of the sub-commands.

𝑐 0 : code L 𝐴 0 𝑐 1 : code L 𝐴 1 ⊨ { { {𝐼} } } 𝑐 0 ∼ 𝑐 1 { { {(𝑚 ′ 0 , 𝑎 0 ), (𝑚 ′ 1 , 𝑎 1 ). 𝐼 (𝑚 ′ 0 , 𝑚 ′ 1 ) ∧ 𝜓 (𝑚 ′ 0 , 𝑎 0 ) (𝑚 ′ 1 , 𝑎 1 )} } } ⊨ { { {𝐼} } } 𝑐 1 ∼ 𝑐 0 { { {(𝑚 ′ 1 , 𝑎 1 ), (𝑚 ′ 0 , 𝑎 0 ). 𝐼 (𝑚 ′ 0 , 𝑚 ′ 1 ) ∧ 𝜓 (𝑚 ′ 0 , 𝑎 0 ) (𝑚 ′ 1 , 𝑎 1 )} } } ⊨ { { {𝐼} } } 𝑐 0 ; 𝑐 1 ∼ 𝑐 1 ; 𝑐 0 { { {(𝑚 ′ 0 , 𝑎 0 ), (𝑚 ′ 1 , 𝑎 1 ). 𝐼 (𝑚 ′ 0 , 𝑚 ′ 1 ) ∧ 𝜓 (𝑚 ′ 0 , 𝑎 0 ) (𝑚 ′ 1 , 𝑎 1 )} } } swap
The swap rule states that if a certain relation on memories 𝐼 is invariant with respect to the execution of 𝑐 0 and 𝑐 1 , then the order in which the commands are executed is not relevant. We used the swap rule in §2.3 in order to swap two independent samplings; in that case the invariant 𝐼 consisted in the equality of memories.

𝑐 0 , 𝑐 ′ 0 : code L 𝐴 0 𝑐 1 : code L ′ 𝐴 1 ⊨ { { {𝜙} } } 𝑐 0 ∼ 𝑐 1 { { {𝜓} } } Pr_code 𝑐 0 = Pr_code 𝑐 ′ 0 ⊨ { { {𝜙} } } 𝑐 ′ 0 ∼ 𝑐 1 { { {𝜓} } } eqDistrL
The eqDistrL rule allows us to replace 𝑐 0 by 𝑐 ′ 0 when both codes have the same denotational semantics as defined by Pr_code, in the sense of §3.2.

𝑐 0 : code L 𝐴 0 𝑐 1 : code L 𝐴 1 ⊨ { { {(𝑚 0 , 𝑚 1 ). 𝜙 (𝑚 0 , 𝑚 1 )} } } 𝑐 0 ∼ 𝑐 1 { { {(𝑚 ′ 0 , 𝑎 0 ), (𝑚 ′ 1 , 𝑎 1 ). 𝜓 (𝑚 ′ 0 , 𝑎 0 ) (𝑚 ′ 1 , 𝑎 1 )} } } ⊨ { { {(𝑚 1 , 𝑚 0 ). 𝜙 (𝑚 0 , 𝑚 1 )} } } 𝑐 1 ∼ 𝑐 0 { { {(𝑚 ′ 1 , 𝑎 1 ), (𝑚 ′ 0 , 𝑎 0 ). 𝜓 (𝑚 ′ 0 , 𝑎 0 ) (𝑚 ′ 1 , 𝑎 1 )} } } symmetry
The symmetry rule simply states that the symmetric judgment holds if the arguments of the preand postconditions are swapped accordingly.

𝑐 0 , 𝑐 1 : N → code L unit 𝑁 : N ∀𝑖. ⊨ { { {𝐼 𝑖} } } 𝑐 0 𝑖 ∼ 𝑐 1 𝑖 { { {𝐼 (𝑖 + 1)} } } ⊨ { { {𝐼 0} } } for_loop 𝑁 𝑐 0 ∼ for_loop 𝑁 𝑐 1 { { {𝐼 (𝑁 + 1)} } } for-loop
The for-loop rule relates two executions of for-loops with the same number of iterations by maintaining a relational invariant through each step of the iteration.

𝑐 0 , 𝑐 1 : code L bool 𝑁 : N ⊨ { { {𝐼 (true, true)} } } 𝑐 0 ∼ 𝑐 1 { { {(𝑚 ′ 0 , 𝑏 0 ), (𝑚 ′ 1 , 𝑏 1 ). 𝑏 0 = 𝑏 1 ∧ 𝐼 (𝑏 0 , 𝑏 1 ) (𝑚 ′ 0 , 𝑚 ′ 1 )} } } ⊨ { { {𝐼 (true, true)} } } do_while 𝑁 𝑐 0 ∼ do_while 𝑁 𝑐 1 { { {(𝑚 ′ 0 , 𝑏 0 ), (𝑚 ′ 1 , 𝑏 1 ). 𝑏 0 = 𝑏 1 = false ∨ 𝐼 (false, false) (𝑚 ′ 0 , 𝑚 ′ 1 )} } } do-while
The do-while rule relates two bounded while loops with bodies 𝑐 0 and 𝑐 1 . Every iteration preserves a relational invariant on memories 𝐼 that depends on a pair of booleans, and the postcondition also stipulates that 𝑐 0 and 𝑐 1 return the same boolean, i.e., 𝑏 0 = 𝑏 1 . This rule follows the pattern of the unbounded do-while rule defined for simple imperative programs by Maillard et al. [START_REF] Maillard | The next 700 relational program logics[END_REF]. We believe that, with some additional work, their ideas could be used to also support unbounded loops in SSProve (see §5.5 for details).

|𝐴|, |𝐵| < 𝜔 𝑓 : 𝐴 → 𝐵 bijective ∀𝑥 . ⊨ { { {𝜙} } } 𝑐 0 𝑥 ∼ 𝑐 1 (𝑓 𝑥) { { {𝜓} } } ⊨ { { {𝜙} } } 𝑎 <$ uniform 𝐴 ; 𝑐 0 𝑎 ∼ 𝑏 <$ uniform 𝐵 ; 𝑐 1 𝑏 { { {𝜓} } } uniform
The uniform rule relates sampling from uniform distributions on finite sets 𝐴 and 𝐵 that are in a bijective correspondence. Note how it applies the bijection 𝑓 in the continuation on the right-hand side.

𝐷 :

Op 𝑥 ∈ |𝐷 | 𝐷 (𝑥) = 1 ⊨ { { {𝜙} } } 𝑐 0 ∼ 𝑐 1 { { {𝜓} } } 𝑦 ∉ freevar(𝑐 0 ) ⊨ { { {𝜙} } } 𝑦 <$ 𝐷 ; 𝑐 0 ∼ 𝑐 1 { { {𝜓} } } dead-sample
The code 𝑦 <$ 𝐷 ; 𝑐 0 samples 𝑦 from the subdistribution 𝐷. If 𝑦 is never used in 𝑐 0 , as indicated by the last premise of the dead-sample rule, then we would like to argue that the sampling constitutes "dead code" and can be ignored. This intuition only holds if 𝐷 is a proper distribution rather than a subdistribution. For instance, if 𝐷 is the null distribution, the sampling behaves like "assert false" and can certainly not be ignored. The premise 𝑥 ∈ |𝐷 | 𝐷 (𝑥) = 1 ensures that 𝐷 is indeed a proper distribution (also known as a "lossless subdistribution"). A uniform distribution over a non-empty set would, for instance, constitute a proper distribution in this sense.

𝐷 : Op 𝑥 ∈ |𝐷 | 𝐷 (𝑥) = 1 ∀𝑦. ⊨ { { {𝜙} } } 𝑐 0 𝑦 ∼ 𝑐 1 { { {𝜓} } } ⊨ { { {𝜙} } } 𝑦 <$ 𝐷 ; 𝑐 0 𝑦 ∼ 𝑐 1 { { {𝜓} } } sample-irrelevant
The sample-irrelevant rule has a similar flavor to dead-sample, as it too requires 𝐷 to be a proper distribution. We assume that 𝑐 0 𝑦 can be related to 𝑐 1 for all values of 𝑦. In other words, the choice of a particular value for 𝑦 is irrelevant for the pre-and postcondition at hand. Therefore, sampling 𝑦 from a proper distribution 𝐷 will likewise allow us to conclude that 𝑐 0 𝑦 is related to 𝑐 1 .

𝑏 0 , 𝑏 1 : bool ⊨ { { {(𝑚 0 , 𝑚 1 ). 𝑏 0 = 𝑏 1 } } } assert 𝑏 0 ∼ assert 𝑏 1 { { {(𝑚 ′ 0 , 𝑎 0 ), (𝑚 ′ 1 , 𝑎 1 ). 𝑏 0 = true ∧ 𝑏 1 = true} } } assert
The assert rule relates two assert commands, as long as "𝑏 0 = 𝑏 1 " holds before the commands. Note that while the precondition is a predicate on initial memories, nothing prevents it form talking about other things such as the booleans 𝑏 0 and 𝑏 1 quantified at the meta-level. It guarantees "𝑏 0 = true ∧ 𝑏 1 = true" afterwards, ignoring the values 𝑎 0 and 𝑎 1 of type unit.

𝑏 : bool

⊨ { { {𝑏 = true} } } assert 𝑏 ∼ return () { { {𝑏 = true} } } assertL
The one-sided assertL rule specifies the behavior an assert with a true boolean, by relating it with return (). Note that if a code fragment 𝑐 0 is shown to be related to an assertion failure ⊨ { { {True} } } 𝑐 0 ∼ assert false { { {𝜓} } }, then 𝑐 0 must necessarily contain an assertion failure as well, i.e., correspond to the null sub-distribution. Indeed the (sound) model of our program logic, explained in §5, gives rise to a total correctness semantics [START_REF] Maillard | The next 700 relational program logics[END_REF] for assertion failures: assertion failures only relate to other assertion failures.

𝑏 0 : bool 𝜅 0 : 𝑏 0 = true → code 𝐴 0 𝑏 1 : bool 𝜅 1 : 𝑏 1 = true → code 𝐴 1 𝑝𝑟𝑒 =⇒ 𝑏 0 = 𝑏 1 𝐻 0 : 𝑏 0 = true, 𝐻 1 : 𝑏 1 = true ⊨ { { {𝜙} } } 𝜅 0 𝐻 0 ∼ 𝜅 1 𝐻 1 { { {𝜓} } } ⊨ { { {𝜙} } } assert 𝑏 0 as ℎ 0 ; 𝜅 0 ℎ 0 ∼ assert 𝑏 1 as ℎ 1 ; 𝜅 1 ℎ 1 { { {𝜓} } } assertD
The assertD rule allows reasoning about the dependent version of assert where the continuation 𝜅 𝑖 is only well-defined if the assertion holds, as described in §3.1. As in the assert rule, the two assertion conditions 𝑏 0 and 𝑏 1 may a priori be different. The precondition 𝜙 has to ensure that 𝑏 0 and 𝑏 1 are either both true or both false. The continuations 𝜅 𝑖 are defined only in case the assertions succeed. Under this assumption, here represented as the hypotheses 𝐻 0 and 𝐻 1 , the continuations 𝜅 𝑖 must be related for the same 𝑝𝑟𝑒 and 𝑝𝑜𝑠𝑡 as the composite statements "assert 𝑏 𝑖 as ℎ 𝑖 ; 𝜅 𝑖 ℎ 𝑖 ". The intuition for the validity of this rule is the following: if 𝑏 𝑖 is true, assert 𝑏 𝑖 as ℎ 𝑖 is defined as 𝜅 𝑖 ℎ 𝑖 and we appeal to the last premise. If 𝑏 𝑖 is false, both composite statements fail and evaluate to the null distribution.

ℓ : L 𝑟 : type ℓ → code L 𝐴 𝑣 : type ℓ ⊨ { { {𝑚 0 = 𝑚 1 } } } put ℓ 𝑣 ; 𝑥 ← get ℓ ; 𝑟 (𝑥) ∼ put ℓ 𝑣 ; 𝑟 (𝑣) { { {(𝑚 ′ 0 , 𝑎 0 ), (𝑚 ′ 1 , 𝑎 1 ). 𝑚 ′ 0 = 𝑚 ′ 1 ∧ 𝑎 0 = 𝑎 1 } } } put-get
The put-get rule states that looking up the value at location ℓ after storing 𝑣 at ℓ results in the value 𝑣. We also have a similar rule to remove a put right before another one at the same location, and one for two get in a row. More interestingly, we provide one-sided rules for get and put which update the pre-or postcondition accordingly.

ℓ : L 0 𝜅 : type ℓ → code L 0 𝐴 0 𝑐 : code L 1 𝐴 1 ∀𝑥 . ⊨ { { {(𝑚 0 , 𝑚 1 ). 𝜙 (𝑚 0 , 𝑚 1 ) ∧ 𝑚 0 [ℓ] = 𝑥} } } 𝜅 (𝑥) ∼ 𝑐 { { {𝜓} } } ⊨ { { {𝜙} } } 𝑥 ← get ℓ ; 𝜅 (𝑥) ∼ 𝑐 { { {𝜓} } } get-lhs ℓ : L 0 𝜅 : type ℓ → code L 0 𝐴 0 𝑣 : type ℓ 𝑐 : code L 1 𝐴 1 ∀𝑚 0 , 𝑚 1 . 𝜙 (𝑚 0 , 𝑚 1 ) =⇒ 𝑚 0 [ℓ] = 𝑣 ⊨ { { {𝜙} } } 𝜅 (𝑣) ∼ 𝑐 { { {𝜓} } } ⊨ { { {𝜙} } } 𝑥 ← get ℓ ; 𝜅 (𝑥) ∼ 𝑐 { { {𝜓} } } get-lhs-rem
With get-lhs, the left-hand side program is able to read from a memory location while we record that information in the precondition. Dually, get-lhs-rem will recover that information from the precondition. We also use the information in the preconditions when dealing with memory invariants such as the one presented in Appendix A for the security proof of KEM-DEM.

The situation is slightly more complicated for one-sided writes because writing might break a postcondition. Typically, writing on only one side when the postcondition ensures that both memory locations are equal would (maybe temporarily) break said postcondition.

ℓ : L 0 𝑣 : type ℓ 𝑐 0 : code L 0 𝐴 0 𝑐 1 : code L 1 𝐴 1 ⊨ { { {(𝑚 0 , 𝑚 1 ). ∃𝑚. 𝜙 (𝑚, 𝑚 1 ) ∧ 𝑚 0 = 𝑚[ℓ ↦ → 𝑣] } } } 𝑐 0 ∼ 𝑐 1 { { {𝜓} } } ⊨ { { {𝜙} } } put ℓ 𝑣 ; 𝑐 0 ∼ 𝑐 1 { { {𝜓} } } put-lhs ℓ : L 0 𝑣 : type ℓ 𝑐 0 : code L 0 𝐴 0 𝑐 1 : code L 1 𝐴 1 ∀ 𝑚 0 𝑚 1 . 𝜙 (𝑚 0 , 𝑚 1 ) =⇒ 𝜙 (𝑚 0 [ℓ ↦ → 𝑣] , 𝑚 1 ) ⊨ { { {𝜙} } } 𝑐 0 ∼ 𝑐 1 { { {𝜓} } } ⊨ { { {(𝑚 0 , 𝑚 1 ). ∃𝑚. 𝜙 (𝑚, 𝑚 1 ) ∧ 𝑚 0 = 𝑚[ℓ ↦ → 𝑣] } } } 𝑐 0 ∼ 𝑐 1 { { {𝜓} } } restore-pre-lhs
Instead put-lhs modifies the precondition to state that the precondition 𝜙 was satisfied by a previous memory state, and that the current memory state is the same except that ℓ now points to 𝑣.

Typically, when 𝜙 is an invariant-such as one stating the equality of the two memories-we relax the precondition temporarily until we reach a new state where it holds again, for instance by having a similar write on the right-hand side. Rule restore-pre-lhs is such an example-although much simplified-of how one can recover the precondition after a write, provided they can prove that the precondition holds after the corresponding update of memory. In SSProve we in fact implement a more general rule accounting for any number of writes on both the left-and right-hand sides.

Several put operations are performed, until one can show that the invariant is preserved by all these memory updates. More generally, we define handy tactics to apply these rules immediately, as well as performing the necessary massaging of goals so that they become applicable. As such we have automation for swapping multiple lines at once and checking that the swap was legal. Moreover, these tactics rely on the hints mechanism of Coq and can thus be extended by the user.

Organization of the relational program logics rules. The rules of the relational program logic are not canonically derived but a few guidelines have been used to come up with them. These guidelines follow three independent criteria: the algebraic criterion, the historical criterion, and the practical criterion. The algebraic criterion follows the idea that the effects employed in the programming language can be modeled using algebraic structures, e.g., monads, and rules corresponding to the standard combinators of this algebraic presentation can be naturally expressed [START_REF] Maillard | The next 700 relational program logics[END_REF]. In particular, equationally presented monads such as the state monad, the exception monad or the Giry probability monad [START_REF] Giry | A categorical approach to probability theory[END_REF][START_REF] Plotkin | Algebraic Operations and Generic Effects[END_REF] naturally induce reasoning rules corresponding to their equational theory [START_REF] Gibbons | Just do it: simple monadic equational reasoning[END_REF]. The algebraic approach, however, falls short of providing a complete solution accounting for the distinction between one-sided and two-sided rules specific to a particular effect-e.g., rules for get and set when considering the state monad. For these rules, the historical presentation follows earlier work on (x)pRHL [START_REF] Barthe | Relational Reasoning via Probabilistic Coupling[END_REF][START_REF] Barthe | Formal certification of code-based cryptographic proofs[END_REF], providing both one-sided and two-sided rules. Finally, the pragmatics of proving relational properties of programs in SSProve pushed for specific presentations of the rules, well tailored to streamlined applications in practice, in particular when considering the specifics of the Coq hosting environment, such as tactic language and incremental proof derivation through interactive use of existential variables and subgoals generation. The redundancy between rules created by these different approaches to relational program logic rules' design is not an issue in practice, since each of these rules is proved against the semantic model presented in §5 rather than assumed axiomatically. The question of completeness of the rules is somehow side-stepped in our setting by having an escape hatch using the relational semantics: in any case, if the rules we provide are not suitable to prove a particular judgment, one can always fall back to the underlying semantic model and prove an additional valid rule at that level. Ultimately, we validate the design of the rules present in SSProve via case studies, ensuring that the chosen set of rules are indeed enough to obtain concrete interesting results.

Proof sketch for Theorem 2.4

If we denote by mem the type of memories, then a binary memory predicate 𝑚 0 : mem, 𝑚 1 : mem ⊢ 𝜓 : P holds on a pair of memories (ℎ 0 , ℎ 1 ), written (ℎ 0 , ℎ 1 ) ⊨ 𝜓 , when 𝜓 (ℎ 0 , ℎ 1 ) holds. Moreover, we say that such predicate is stable on sets of locations L 0 and L 1 when for all ℎ 0 , ℎ 1 such that (ℎ 0 , ℎ 1 ) ⊨ 𝜓 , we have for all memory locations 𝑙, such that 𝑙 ∉ L 0 and 𝑙 ∉ L 1 , that (1)

ℎ 0 [𝑙] = ℎ 1 [𝑙].
(2) for all 𝑣, (ℎ 0 [𝑙 ↦ → 𝑣] , ℎ 1 [𝑙 ↦ → 𝑣]) ⊨ 𝜓 . In other words, on locations outside of L 0 and L 1 , 𝜓 must ensure equality of corresponding values and nothing else.

When we want to prove that two packages with the same interface are perfectly indistinguishable, we will assume that we have a stable predicate on the locations of the packages, and moreover, that this predicate is an invariant on the different operations of the interface. This invariance of the predicate is the reason why 𝜓 appears both as a pre-and postcondition in Theorem 2.4. Notice that stable predicates do not impose conditions on the intermediate states of each procedure in the interface of Theorem 2.4, e.g. two related procedures may differ in their internal order of updates, as long as the final results of computations are related.

Before giving the proof sketch for Theorem 2.4, we state a theorem that is also proved in Coq and relates the probabilistic relational program logic with the probabilistic semantics. Theorem 4.1. Given values 𝑎, 𝑏, if two pieces of code 𝑐 0 , 𝑐 1 are such that

⊨ { { {𝜓} } } 𝑐 0 ∼ 𝑐 1 { { {𝜙} } },
𝜓 holds on the initial memories, and for all 𝑚 ′ 0 , 𝑚 ′ 1 , 𝑥 and 𝑦 we have that 𝜙 (𝑚 ′ 0 , 𝑥) (𝑚 ′ 1 , 𝑦) =⇒ (𝑥 = 𝑎 ⇐⇒ 𝑦 = 𝑏) , then we have

Pr[𝑎 ← 𝑐 0 ] = Pr[𝑏 ← 𝑐 1 ] .
We are now ready to outline the proof for Theorem 2.4.

Proof sketch of Theorem 2.4. We want to prove that for each adversary A we have the equality 𝛼 (𝐺 01 ) (A) = 0, i.e.,

Pr true ← A • 𝐺 0 -Pr true ← A • 𝐺 1 = 0.
Using the hypothesis and the fact that the predicate 𝜓 is a stable invariant, i.e., stable on sets of locations mem(𝐺 0 ) and mem(𝐺 1 ), we perform an induction on the code of the procedure A.Run, to establish

⊨ { { {𝜓} } } A • 𝐺 0 .Run() ∼ A • 𝐺 1 .Run() { { {(𝑚 ′ 0 , 𝑏 0 ), (𝑚 ′ 1 , 𝑏 1 ). 𝑏 0 = 𝑏 1 ∧ 𝜓 (𝑚 ′ 0 , 𝑏 0 ) (𝑚 ′ 1 , 𝑏 1 )} } }.
As the induction proceeds, the rules from §4.1 are used to prove each case. We illustrate the get case, which after applying the seq rule with respect to the continuation, and using the inductive hypothesis, reduces to the following judgment:

⊨ { { {𝜓} } } get l (λx.return x) ∼ get l (λx.return x) { { {(𝑚 ′ 0 , 𝑣 0 ), (𝑚 ′ 1 , 𝑣 1 ). 𝑣 0 = 𝑣 1 ∧ 𝜓 (𝑚 ′ 0 , 𝑣 0 ) (𝑚 ′ 1 , 𝑣 1 )} } }
As 𝜓 is stable, we know that the result of get on the left and on the right will coincide (i.e., 𝑚 0 [𝑙] = 𝑚 1 [𝑙]), because 𝑙 ∉ L 0 and 𝑙 ∉ L 1 as 𝑙 is a location used in the adversary's code (remember we are performing induction on the adversary's code), and we explicitly asked for the adversary memory mem(A) to be disjoint from mem(𝐺 0 ) and mem(𝐺 1 ). As the memory was not changed, the invariant 𝜓 still holds on the final memory.

As the predicate 𝜓 holds on the initial memories, and the postcondition 𝑏 0 = 𝑏 1 ∧ 𝜓 implies that 𝑏 0 = 𝑡𝑟𝑢𝑒 ⇐⇒ 𝑏 1 = 𝑡𝑟𝑢𝑒, we know from Theorem 4.1 that

Pr true ← A • 𝐺 0 = Pr true ← A • 𝐺 1 ,
and therefore the advantage is 0. □

SEMANTIC MODEL AND SOUNDNESS OF RULES

We build a semantic model validating the rules of the effectful relational program logic from §4.

The construction of the model builds upon an effect-modular framework [START_REF] Maillard | The next 700 relational program logics[END_REF], instantiating it with probabilities, simple failures, and global state. We first give in §5.1 an overview of the framework of Maillard et al. [START_REF] Maillard | The next 700 relational program logics[END_REF]. We then informally explain how we apply it in order to (1) obtain a model for a probabilistic relational program logic in §5.2 and (2) enrich it with state in §5.3. The categorical constructions underlying the framework are explained in §5.4, together with the extensions that we need in this work. Finally, in §5.5 we compare this methodology to other approaches for modelling relational program logics.

Relational effect observation

The aforementioned framework builds upon a monadic representation of effects to provide sound semantics to a large class of relational program logics. As we shall see, this class notably contains logics for reasoning about cryptographic code: code that can manipulate state and sample randomly (see §4.1). A generic relational program logic 𝑟 L is a deductive system with a relational judgment ⊨ 𝑐 0 ∼ 𝑐 1 { 𝑤 } asserting that pairs of effectful code fragments 𝑐 0 , 𝑐 1 behave according to a given relational specification 𝑤 connecting the two computations. The exact shape of code and specifications appearing in such a judgment can vary depending on what programming language and logic are considered. The recipe laid out by Maillard et al. [START_REF] Maillard | The next 700 relational program logics[END_REF] stems from the realization that not only effectful code can be modelled using monads, but specifications can too, and we can build semantics for 𝑟 L using a so-called relational effect observation in three steps:

(1) Model the effects involved in the considered left and right programs as monads 𝑀 0 and 𝑀 1 .

(2) Turn the collection of relational specifications 𝑤 into a relational specification monad (𝐴 0 , 𝐴 1 ) ↦ → 𝑊 (𝐴 0 , 𝐴 1 ) where 𝐴 0 corresponds to the return type of the left program, and 𝐴 1 the return type of the right program. The set 𝑊 (𝐴 0 , 𝐴 1 ) should be ordered by entailment of specifications, written 𝑤 ≤ 𝑤 ′ . (3) Finally, find an appropriate relational effect observation 𝜃 𝐴 0 𝐴 1 :

𝑀 0 𝐴 0 × 𝑀 1 𝐴 1 → 𝑊 (𝐴 0 , 𝐴 1 )
mapping a pair of monadic computations in 𝑀 0 𝐴 0 × 𝑀 1 𝐴 1 to a relational specification in 𝑊 (𝐴 0 , 𝐴 1 ), and preserving the monadic features present on both sides. Once a relational effect observation 𝜃 is specified we define a semantic judgment for 𝑟 L as follows:

⊨ 𝜃 𝑐 0 ∼ 𝑐 1 { 𝑤 } ⇐⇒ 𝜃 𝐴 0 𝐴 1 (𝑐 0 , 𝑐 1 ) ≤ 𝑤
where 𝑐 𝑖 : 𝑀 𝑖 𝐴 𝑖 and 𝑤 : 𝑊 (𝐴 0 , 𝐴 1 ).

A typical example of a relational specification monad is the relational backward predicate transformer monad BP(𝐴 0 , 𝐴 1 ) := (𝐴 0 ×𝐴 1 →P) → P, where P is the type of propositions. Intuitively a backward predicate transformer 𝑤 : BP(𝐴 0 , 𝐴 1 ) maps a relational postcondition 𝜙 to a precondition 𝑤 𝜙 sufficient to ensure 𝜙 on the result of the executions of code fragments 𝑐 0 , 𝑐 1 respecting 𝑤 (i.e., for which ⊨ 𝜃 𝑐 0 ∼ 𝑐 1 { 𝑤 } for some 𝜃 ). The preorder on BP(𝐴 0 , 𝐴 1 ) is given by reverse pointwise implication. For two backward predicate transformers 𝑤 1 , 𝑤 2 : BP(𝐴 0 , 𝐴 1 ), we say that 𝑤 1 ≤ 𝑤 2 when ∀𝜙 . 𝑤 2 𝜙 ⇒ 𝑤 1 𝜙. Every pre-/postcondition pair (𝑝𝑟𝑒, 𝑝𝑜𝑠𝑡) can systematically be translated into a single backward predicate transformer toBP(𝑝𝑟𝑒, 𝑝𝑜𝑠𝑡): toBP(𝑝𝑟𝑒, 𝑝𝑜𝑠𝑡) := 𝜆 (𝜙 : 𝐴 0 × 𝐴 1 →P). 𝑝𝑟𝑒 ∧ ∀𝑎. 𝑝𝑜𝑠𝑡 𝑎 ⇒ 𝜙 𝑎 : BP(𝐴 0 , 𝐴 1 ) Note that BP does not form a monad: it takes two types 𝐴 0 , 𝐴 1 as input but only returns one (𝐴 0 × 𝐴 1 →P) → P. Yet BP somehow still behaves as a monad because we can equip it with bind and return operations satisfying equations akin to the standard monad laws. This is one of the reasons why our precise definitions of relational specification monad and relational effect observation are centered around the notion of relative monad instead, as discussed in [START_REF] Maillard | The next 700 relational program logics[END_REF] and explained here in §5.4.

Effect observation for probabilities and failures

The technique above can be exploited to build a model for a probabilistic relational program logic. We model probabilistic code using a free monad F Pr over a probabilistic signature, reusing code L,𝐼 mentioned in §3.1, where we require that only sampling operations are performed. This code can be assigned a probabilistic semantics using the monad of subdistributions [START_REF] Audebaud | Proofs of Randomized Algorithms in Coq[END_REF][START_REF] Giry | A categorical approach to probability theory[END_REF], following the track of §3.2, but ignoring considerations around state. This semantics assignment can in fact be seen as a monad morphism 𝛿 : F Pr → SD.

Specifications and effect observation. To model specifications for probabilistic code we use the relational specification monad BP of backward predicate transformers, defined above. The relational effect observation 𝜃 Pr is based on the notion of probabilistic coupling. A coupling 𝑑 : coupling(𝑑 0 , 𝑑 1 ) of two subdistributions 𝑑 0 : SD(𝐴 0 ) and 𝑑 1 : SD(𝐴 1 ) is a subdistribution over 𝐴 0 × 𝐴 1 such that its left and right marginals correspond to 𝑑 0 and 𝑑 1 respectively. For 𝑑 𝑖 : SD(𝐴 𝑖 ) two subdistributions we define 𝜃 ′ Pr : SD × SD → BP by: 𝜃 ′ Pr 𝐴 0 𝐴 1 (𝑑 0 , 𝑑 1 ) := 𝜆(𝜙 : 𝐴 0 × 𝐴 1 → P). ∃(𝑑 : coupling(𝑑 0 , 𝑑 1 )). ∀𝑎 0 𝑎 1 . 𝑑 (𝑎 0 , 𝑎 1 ) > 0 ⇒ 𝜙 (𝑎 0 , 𝑎 1 ).

We moreover turn the domain of 𝜃 ′ Pr into a product of free monads by setting

𝜃 Pr := 𝜃 ′ Pr • 𝛿 2 : F Pr × F Pr → BP.
Intuitively, if 𝑤 : 𝐵𝑃 (𝐴 0 , 𝐴 1 ) is obtained out of a (𝑝𝑟𝑒, 𝑝𝑜𝑠𝑡) pair, the semantic judgment ⊨ 𝜃 𝑃𝑟 𝑐 0 ∼ 𝑐 1 { 𝑤 } holds when one can find a coupling 𝑑 of 𝛿 (𝑐 0 ), 𝛿 (𝑐 1 ) whose support validates 𝑝𝑜𝑠𝑡 whenever 𝑝𝑟𝑒 is valid. Our probabilistic model ⊨ 𝜃 𝑃𝑟 𝑐 0 ∼ 𝑐 1 { 𝑤 } validates state-free accounts of several rules of §4.1. First, since the subdistribution monad is commutative (sampling operations always commute), our semantics validates a state-free variant of the swap rule. Second, as it is often the case for an arbitrary effect observation, symmetric rules like uniform involving similar effectful operations on both sides (here: 𝑎 <$ uniform 𝐴) are validated as well. Third, failing assertions at type 𝐴 can be modelled using the null subdistribution on 𝐴, and this interpretation allows us to validate the assert rule in our model. Fourth, a state-free variant of the reflexivity rule can be established by building, for any subdistribution 𝑠, a coupling 𝑑 : coupling(𝑠, 𝑠) of 𝑠 with itself. Fifth, any relational effect observation 𝜃 validates a rule like seq. Such a rule is essentially a syntactic formulation of the fact that 𝜃 should preserve the monadic composition, which is true by definition.

The implementation of the relational effect observation 𝜃 Pr in Coq depends on a mathematical theory of couplings and of their interaction with probabilistic programs that we developed. This theory relies internally upon the mathcomp-analysis library [START_REF] Affeldt | Competing inheritance paths in dependent type theory: a case study in functional analysis[END_REF][START_REF] Affeldt | Analysis library compatible with Mathematical Components[END_REF], particularly on their formalization of real numbers, subdistributions and discrete integrals.

Adding state

To extend this first model to stateful code and state-aware specifications, we adapt to our setting the classical notion of state monad transformer [START_REF] Liang | Monad Transformers and Modular Interpreters[END_REF]. A monad transformer maps monads 𝑀 to monads T 𝑀 and monad morphisms 𝜃 to monad morphisms T 𝜃 . In particular, the state monad transformer takes as input a monad 𝑀 and a fixed set of states 𝑆 and produces a monad with underlying carrier StT 𝑀 (𝐴) = 𝑆 → 𝑀 (𝐴 × 𝑆) with additional ability to read and write elements of 𝑆. Besides, a monad transformer comes equipped with a family of liftings lift T : ∀𝑀. 𝑀 → T 𝑀 coercing any computation in the original monad 𝑀 to a computation in the extended effectful environment T 𝑀. We generalize this to specification monads and build modularly an effect observation 𝜃 Pr,St on top of 𝜃 Pr :

𝜃 ′ Pr,St := StT 𝜃 Pr : StT(F 2
Pr ) (𝐴 0 , 𝐴 1 ) → StT(BP) (𝐴 0 , 𝐴 1 ) using two sets of global states 𝑆 0 , 𝑆 1 for the left and right, where:

StT(F 2 Pr ) (𝐴 0 , 𝐴 1 ) := 𝑆 0 × 𝑆 1 → F Pr (𝐴 0 × 𝑆 0 ) × F Pr (𝐴 1 × 𝑆 1 ), StT(BP) (𝐴 0 , 𝐴 1 ) := (𝐴 0 × 𝑆 0 × 𝐴 1 × 𝑆 1 → P) → 𝑆 0 × 𝑆 1 → P.
Following the definition of 𝜃 Pr in §5.2, we further extend 𝜃 ′ Pr,St by turning its domain into a product of free monads F 2 Pr,St := F Pr,St × F Pr,St over a stateful and probabilistic signature. This extension is obtained from 𝜃 ′ Pr,St by precomposition with the mapping mentioned in §3.2:

𝜃 Pr,St := 𝜃 ′ Pr,St • Pr_code 2 .
Using the liftings lift StT provided by StT, we can build from any purely probabilistic relational judgment ⊨ 𝜃 Pr 𝑐 0 ∼ 𝑐 1 { 𝑤 }, a relational judgment ⊨ 𝜃 Pr,St 𝑐 0 ∼ 𝑐 1 lift StT 𝑤 in the state-aware model. This correspondence can be shown to form an embedding of logics: for every 𝑐 0 , 𝑐 1 , 𝑤 free from state manipulation, derivations of ⊨ 𝜃 Pr,St 𝑐 0 ∼ 𝑐 1 lift StT 𝑤 are in bijective correspondence with derivations of ⊨ 𝜃 Pr 𝑐 0 ∼ 𝑐 1 { 𝑤 }. The proof of this latter fact is simplified by the modularity of the construction. This modularity is moreover reflected in the way 𝜃 Pr,St (𝑐 0 , 𝑐 1 ) evaluates. A first pass converts stateful operations of 𝑐 0 , 𝑐 1 and yields state-passing probabilistic code. A second pass interprets the remaining sampling operations and yields state-transforming subdistributions. Lastly a third pass uses 𝜃 𝑃𝑟 and yields the expected specification 𝜃 Pr,St (𝑐 0 , 𝑐 1 ) : StT(BP) (𝐴 0 , 𝐴 1 ). The semantic judgment ⊨ 𝜃 Pr,St 𝑐 0 ∼ 𝑐 1 { 𝑤 } obtained out of 𝜃 Pr,St validates all of the rules of our relational program logic (including §4.1).

Categorical foundations of the framework

Our semantics relies on the notion of relational effect observation ( §5.1), and on our ability to apply a suitable state transformer to them ( §5.3). In this section, we provide categorical definitions for those notions. Our Coq formalization of the semantics is essentially a formal version of the theory laid out here. Note that Coq types and functions between them form a category that we call Type. We will also use the category PreOrder of types equipped with a preorder structure (reflexive, transitive relation), and monotone functions.

Computations and specifications as order-enriched relative monads. We are interested in modelling probabilistic programs using monads. Yet, in our constructive setting probabilistic computations fail to form a monad. Indeed, our Coq formalization relies on the mathcomp-analysis library which defines the type of subdistributions SD(𝐴) (see §3.2) only when 𝐴 is a "choiceType", that is, a type equipped with an enumeration function for each of its decidable subtypes. This extra choice structure is crucial to define a well-behaved notion of discrete integral on 𝐴, and consequently of subdistribution on 𝐴. Beyond the discrepancy between the domain and codomain of SD, it is still possible to endow it with slightly modified versions of the expected bind and return operations, that satisfy laws comparable to the standard monad laws. Fortunately, Altenkirch et al. [START_REF] Altenkirch | Monads need not be endofunctors[END_REF] explain well how these superficial obstructions due to a mismatch between the domain and codomain of a monad-like structure can be solved using the closely related notion of a relative monad instead. As a trivial example, any monad 𝑀 : C → C can be seen as a relative monad over the identity functor Id C . Writing chTy for the category of choice types (choiceType), we are able to package SD : chTy → Type as a monad relative to the inclusion functor chTy → Type forgetting the extra choice structure. Similarly the probabilistic code monad F Pr must actually be restricted to chTy and only forms a relative monad F Pr : chTy → Type over the inclusion functor.

Regarding specifications, relational specification monads W fail to form monads as well. Indeed, 𝑊 : Type × Type → PreOrder expects two types 𝐴 0 , 𝐴 1 as input but only returns one 𝑊 (𝐴 0 , 𝐴 1 ), which is moreover pre-ordered. Again, it turns out that relational specification monads 𝑊 (including BP) can be seen as relative monads, over the discrete product functor dprod mapping two types to their product seen as a trivial preorder:

dprod : Type × Type → PreOrder 𝐴 0 , 𝐴 1 ↦ → 𝐴 0 × 𝐴 1 .
Specializing the definition of a relative monad with 𝐽 = dprod, the bind and return operations of 𝑊 take the following form:

return W : 𝐴 0 × 𝐴 1 → 𝑊 (𝐴 0 , 𝐴 1 ) bind W : (𝐴 0 × 𝐴 1 → 𝑊 (𝐵 0 , 𝐵 1 )) → 𝑊 (𝐴 0 , 𝐴 1 ) → 𝑊 (𝐵 0 , 𝐵 1 )
To soundly model relational program logics, the bind W operation of the relational specification monad being used should be monotonic in both arguments. In our setting, we can in fact easily express that condition by requiring all categorical constructions to be order-enriched [START_REF] Katsumata | Preorders on Monads and Coalgebraic Simulations[END_REF][START_REF] Kelly | Basic Concepts of Enriched Category Theory[END_REF][START_REF] Rauch | Generic Hoare Logic for Order-Enriched Effects with Exceptions[END_REF].

For the sake of readability, we ignore the trivial considerations arising from this enrichment and consider that all the constructions we are dealing with are implicitly order-enriched. Summing up, in our setting:

• Pairs of computations are modelled by a product 𝑀 0 × 𝑀 1 of Type-valued (order-enriched) relative monads. • Specifications are modelled using a relational specification monad 𝑊 , i.e., a (order-enriched) relative monad over the discrete product functor dprod : Type × Type → PreOrder. For instance, the domain and codomain of the relational effect observation 𝜃 Pr defined in §5.2 form respectively a product of Type-valued relative monads, and a relational specification monad. dom(𝜃 Pr ) is F Pr × F Pr : chTy × chTy → Type × Type cod(𝜃 Pr ) is BP : Type × Type → PreOrder Relational effect observations. Consider 𝑀 0 , 𝑀 1 two Type-valued relative monads with base functors 𝐽 0 , 𝐽 1 respectively. Let 𝑊 be a relational specification monad. The relative monads 𝑀 0 × 𝑀 1 and 𝑊 organize in the following configuration:

dom(𝑀 0 ) × dom(𝑀 1 )
Type 2

Type 2 PreOrder

𝑀 0 ×𝑀 1 𝑊 𝐽 0 ×𝐽 1 dprod
A relational effect observation 𝜃 : 𝑀 0 × 𝑀 1 → 𝑊 is a collection of mappings

𝜃 𝐴 0 𝐴 1 : 𝑀 0 𝐴 0 × 𝑀 1 𝐴 1 → 𝑊 (𝐽 0 𝐴 0 , 𝐽 1 𝐴 1 )
preserving the bind and return operations of 𝑀 0 , 𝑀 1 up to inequalities:

𝜃 (return 𝑀 0 𝑎 0 , return 𝑀 1 𝑎 1 ) ≤ return 𝑊 (𝑎 0 , 𝑎 1 ) (4)
𝜃 (bind

𝑀 0 𝑓 0 𝑚 0 , bind 𝑀 1 𝑓 1 𝑚 1 ) ≤ bind 𝑊 (𝜃 • (𝑓 0 , 𝑓 1 )) 𝜃 (𝑚 0 , 𝑚 1 ) (5)
An instance of relational effect observation is of course given by 𝜃 Pr . Note that 𝜃 Pr validates those inequalities but fails to validate them as equalities.

In our development, relational effect observations 𝜃 : 𝑀 0 × 𝑀 1 → 𝑊 are defined as special cases of lax morphisms between order-enriched relative monads. We refer the interested reader to our formalization 7 for a precise definition of this notion. In the remainder of this section, we explain how to extend relative monads and lax morphisms between them with state. In particular, this extension will apply to relational effect observations such as 𝜃 Pr .

Transforming a relative monad with an appropriate left adjunction. It is a standard result that every adjunction induces a monad and that every monad is induced by a family of adjunctions (see [START_REF] Mac | Categories for the Working Mathematician[END_REF], chapter 6). A similar kind of correspondence holds between left 𝐽 -relative adjunctions on one side, and 𝐽 -relative monads on the other. The two following definitions appear in [START_REF] Altenkirch | Monads need not be endofunctors[END_REF]. It is indeed a category exactly thanks to the monad laws of 𝑀. Moreover there exist functors 𝐿 𝑀 , 𝑅 𝑀 in the following configuration Kl(𝑀)

I C 𝐿 𝑀 𝑅 𝑀 𝐽 𝑀
that form a 𝐽 -relative adjunction inducing 𝑀, that is, 𝑀 = 𝑅 𝑀 𝐿 𝑀 .

In this work we introduce the following notion.

Definition 5.4 (Transforming adjunction). Consider functors 𝐽, 𝐿 ♭ , 𝑅 in the following configuration:

I C I C 𝐽 𝐽 𝐿 ♭ 𝑅
An adjunction 𝛼 : 𝐽 𝐿 ♭ 𝐽 ⊣ 𝑅 is called a transforming adjunction.

If I is cartesian, C is cartesian closed, and 𝐽 preserves cartesian products, the following configuration gives rise to a transforming adjunction 𝜎 : 𝐽 • (-× 𝑆) 𝐽 ⊣ 𝑆 → -, which we suggestively call "state-transforming adjunction". Note that the 𝐽 -relative monad induced by this adjunction 𝑋 ↦ → 𝑆 → 𝐽 (𝑋 × 𝑆) is a 𝐽 -shifted version of a standard state monad.

I C I C

-×𝑆 𝑆→-𝐽 𝐽 Theorem 5.5 (Relative transformer). Given a 𝐽 -relative monad 𝑀 : I → C "sitting" on a transforming adjunction 𝛼 : 𝐽 𝐿 ♭ 𝐽 ⊣ 𝑅, the composition 𝑅𝑀𝐿 ♭ is also a 𝐽 -relative monad. We call it the relative monad transformed by 𝛼 and denote it as T 𝛼 𝑀.

Proof Sketch. We can factorize 𝑀 through its Kleisli category as shown in Definition 5.3 to obtain T 𝛼 𝑀 := 𝑅𝑀𝐿 ♭ = 𝑅𝑅 𝑀 𝐿 𝑀 𝐿 ♭ and observe that 𝐿 𝑀 𝐿 ♭ 𝐽 ⊣ 𝑅𝑅 𝑀 , meaning that T 𝛼 𝑀 is the relative monad induced by the latter adjunction. □

Adding state to a 𝐽 -relative monad 𝑀 consists in applying the above theorem with the statetransforming adjunction 𝜎 defined above to obtain StT 𝑀 := 𝑇 𝜎 𝑀. In particular, this is how the domain and codomain of StT(𝜃 Pr ) from §5.3 are defined.

Transforming lax morphisms. In order to transform lax morphisms of relative monads (such as 𝜃 Pr ) we follow the same methodology as in the previous paragraph. Various non-standard categorical notions are at play under the hood: lax morphisms of left relative adjunctions, lax functors, and lax natural transformations. Informally, let 𝜃 : 𝑀 → 𝑊 be a lax morphism of relative monads. Let 𝛼 be a transforming adjunction for both 𝑀 and 𝑊 . Then 𝜃 induces a lax morphism between the Kleisli adjunctions of its domain and codomain: Kl(𝜃 ) : (𝐿 𝑀 𝐽 ⊣ 𝑅 𝑀 ) -→ (𝐿 𝑊 𝐽 ⊣ 𝑅 𝑊 ) Kl(𝜃 ) can then be pasted with an appropriate cell to obtain a lax morphism between the transformed adjunctions, which ultimately induces a morphism T 𝛼 𝜃 : T 𝛼 𝑀 → T 𝛼 𝑊 between the transformed relative monads. Adding state to a relational effect observation 𝜃 now consists in applying the above with the state-transforming adjunction 𝜎. This is how we can obtain StT(𝜃 Pr ) := T 𝜎 𝜃 Pr in a modular way.

Comparing approaches to semantic models for relational program logics

We use the semantic framework of Maillard et al. [START_REF] Maillard | The next 700 relational program logics[END_REF] based on effect observations to obtain a formal and foundational approach to relational program logics for cryptographic code. In this section, we compare this methodology to other approaches for modelling relational program logics.

The Foundational Cryptography Framework (FCF) [START_REF] Petcher | The Foundational Cryptography Framework[END_REF] develops machine-checked proofs of cryptographic code in the Coq proof assistant. Computations are modelled as elements of a free monad, then interpreted as distributions. This denotational model is subsequently used to derive a program logics using couplings. The approach we take is similar, but we paid special attention to the intermediate monadic structures involved. For instance, FCF distinguishes the type of simple computations Comp 𝑅 with result value in 𝑅 from the type of computations with access to some oracle OracleComp 𝐼 𝑂 𝑅. The latter provides operations to query an oracle with a given value in 𝐼 and obtain results in 𝑂 of an oracle call that are not found in simple computations. We rely on the genericity of free monads at the level of packages to encode both the simple computations and computations with oracles in a single uniform type of code, using the parameterized operations to provide oracle queries for instance. State passing is done explicitly in FCF, while we prefer a more abstract presentation using a state monad transformer. As a result, we obtain a conceptually comfortable decomposition of our computational monads and specifications, at the price of additional work to define the few components that we need for verification of cryptographic code.

Although the implementation of EasyCrypt does not have a proper foundational backend per se, many rules of its probabilistic relational Hoare logic (pRHL) were proved sound in Coq in a project called XHL with respect to a model [START_REF] Strub | XHL[END_REF], parts of which have been merged into mathcomp-analysis [START_REF] Affeldt | Analysis library compatible with Mathematical Components[END_REF]. Our own development relies on these very same definitions and lemmas for the probabilistic aspect of the relational specification monads and the underlying theory of couplings. Our contribution here, forced by the organization of the framework of Maillard et al. [START_REF] Maillard | The next 700 relational program logics[END_REF], is to show formally that the various lemmas proved in the library indeed build instances of the monadic abstractions that are not explicated in the original development. Amongst the technical difficulties that appeared in that operation, we should mention the fact that distributions are only built-in mathcomp-analysis for types equipped with a certain choice structure, reflecting the constructive nature of Coq. However, we cannot endow distributions with such a choice structure, and in particular, distributions do not form monads, but they do form relative monads over the functor forgetting the choice structure (see §5.4). Note that although the definition of the semantic judgment ⊨ 𝜃 Pr,St 𝑐 0 ∼ 𝑐 1 { 𝑤 } can seem abstract at first, it ultimately reduces to a direct formulation equivalent to the one underlying XHL.

CertiCrypt is a predecessor of EasyCrypt embedded directly in Coq and our foundational approach is closer in spirit to CertiCrypt than to its successor. CertiCrypt's Coq code employs an elaborate definition of probabilistic Relational Hoare Logic judgments in terms of approximate couplings, based on the ALEA library [START_REF] Audebaud | Proofs of Randomized Algorithms in Coq[END_REF][START_REF] Paulin-Mohring | ALEA Coq Library[END_REF], which directly offers support for bounding the distance between the distributions of two probabilistic programs. It also features a memory model distinguishing between local and global variables, providing the ability to give a direct semantics for first-order procedure calls with local state in the form of "stack frames". This memory model could be employed easily in our account of the state relative monad transformer.

CertiCrypt, EasyCrypt and FCF provide some support for unbounded while loops, ultimately relying at the semantic level on the fact that distributions take values in a complete lattice, namely the real numbers, and using standard fixpoint theorems to obtain an interpretation of arbitrary loops. Our semantic account could also support such an extension, as witnessed by the semantics Maillard et al. [START_REF] Maillard | The next 700 relational program logics[END_REF] construct for a simple Imp language with unbounded loops.

While a direct ad-hoc definition of the model is comparatively simpler to implement, our categorical approach aims to provide more modularity, with the potential to account for multiple effects. This modular approach makes explicit that the model can be restricted to one validating a solely probabilistic program logic ( §5.2). Moreover, it should be possible to extend our stateful model with other effects using a similar range of algebraic techniques. However, as things stand now, incorporating new effects in our relational program logic and its associated semantics can only be done on a case by case basis. Developing and using the framework required a high proof effort, in particular to manipulate the various layers of abstractions when proving concrete statements, such as the soundness of rules of the relational program logics specific to the effects involved. Further engineering work would be needed to make efficient use of the factorisation provided by abstraction and bring this approach to a competitive level compared to the simpler direct approach of FCF [START_REF] Petcher | The Foundational Cryptography Framework[END_REF] and XHL [START_REF] Strub | XHL[END_REF].

CASE STUDY: KEM-DEM

In order to better demonstrate the practicality of our tool we formalized a more involved public key encryption scheme, KEM-DEM originally proposed by Cramer and Shoup [START_REF] Cramer | Design and Analysis of Practical Public-Key Encryption Schemes Secure against Adaptive Chosen Ciphertext Attack[END_REF], and used for instance in the CryptoBox protocol [START_REF] Daniel | Cryptography in NaCl[END_REF]. KEM-DEM consists in the composition of a key encapsulation mechanism (KEM) and a data encryption mechanism (DEM), and it can be proved to be indistinguishable from random under chosen ciphertext attacks (IND-CCA), as long as both the KEM and DEM are also IND-CCA schemes.

Our formalization of KEM-DEM showcases high-level SSP arguments that are not present in our previous examples such as parallel composition, the identity package, and the interchange law. Furthermore, we make a more extensive use of our probabilistic relational framework. In particular, we have to account for more interesting invariants than the mere equality of state we were using previously.

Our mechanized proof of KEM-DEM faithfully follows the single-instance security proof done on paper by Brzuska et al. [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF]Section 4]. In fact, while conducting the proof in SSProve, we were able to find-in conjunction with the authors of [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF]-a flaw in their argument which has led them to propose a revised version of their theorem and its corresponding proof. This section describes the revised proof, which we formalized in SSProve.

The KEY package

The KEM-DEM protocol involves the use of a symmetric key to encrypt the actual data that is going to be sent. The KEY package is used for generating, storing and accessing such a key.

All our statements, as well as the KEY package itself, are parameterized over a type of symmetric keys and distribution keyD for generating them. In this respect we generalize [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF], which uniformly samples over bit-strings of a given length. We give the KEY package in Figure 14.

Next we consider packages that may rely on KEY either for storage/generation or for access of an otherwise set key; we will later see the KEM and DEM as instances of those. We call the former keying and the latter keyed games. More formally, a keying game K 𝑏 is given by a core keying game CK 𝑏 with import(CK 0 ) = {Set}, and import(CK 1 ) = {Gen}, and Get ∉ export(CK 𝑏 ), while a keyed game 𝐷 𝑏 is given by a core keyed game CD 𝑏 such that import(CD 𝑏 ) = {Get}, and Gen ∉ export(CD 𝑏 ). They are graphically represented in Figure 15 indicate that the import is either Gen or Set depending on the secret bit 𝑏) and defined as follows:

K 𝑏 = (CK 𝑏 ∥ ID {Get} ) • KEY D 𝑏 = (ID {Gen} ∥ CD 𝑏 ) • KEY
The import and export interface conditions stated above ensure that these packages are meaningful. As we will see, we will define the KEM package as a core keying game, and the DEM package as a core keyed game. From that fact alone we will be able to derive security bounds on games that combine them as evidenced by the following lemma. Lemma 6.1 (Single key). Given a keying game pair 𝐾 01 and a keyed game pair 𝐷 01 as above, we have the following inequalities for any distinguisher D:

𝛼 ((CK 0 ∥ CD 0 ) • KEY, (CK 1 ∥ CD 1 ) • KEY) (D) ≤ 𝛼 (K 01 ) (D • (ID export(CK) ∥ CD 0 )) + 𝛼 (D 01 ) (D • (CK 1 ∥ ID export(CD) )) 𝛼 ((CK 0 ∥ CD 0 ) • KEY, (CK 0 ∥ CD 1 ) • KEY) (D) ≤ 𝛼 (K 01 ) (D • (ID export(CK) ∥ CD 0 )) + 𝛼 (D 01 ) (D • (CK 1 ∥ ID export(CD) )) + 𝛼 (K 01 ) (D • (ID export(CK) ∥ CD 1 ))
Proof. We once again make use of Lemma 2.2 and Lemma 2.3 for game-hopping but also of the interchange and identity laws. We will represent the sequence graphically. The packages that we consider are represented in Figure 16 with potentially different instances of 𝑏 and 𝑐. For the first inequality we want to relate the figure where 𝑏 = 0 and 𝑐 = 0 to the case where 𝑏 = 1 and 𝑐 = 1. To accomplish this we perform the reductions found in Figure 17 which correspond to applications of the identity and interchange laws to the package of Figure 16, and thus they represent equal packages. For instance, we first change CK 0 to CK 1 in (CK 0 ∥ CD 0 ) • KEY by "pushing" CD 0 to the left (i.e., using the reduction on top), meaning we obtain equal package (ID export(CK) ∥ CD 0 ) • K 0 . We then hop to (ID export(CK) ∥ CD 0 ) • K 1 , incurring the term 𝛼 (K 01 ) (D • (ID export(CK) ∥ CD 0 )) in the inequality, and then proceed back to (CK 1 ∥ CD 0 ) • KEY by doing the inverse of the reduction. The whole proof proceeds in a similar way. The second inequality is a consequence of the first one where we additionally de-idealize the core keying package (CK 1 In order to be as general as possible, we will assume we are given KEM and DEM schemes. As stated earlier, the KEM will generate a symmetric key and encrypt it using an asymmetric scheme. The DEM will then use that symmetric key to encrypt the data to be sent. To that effect we assume we are given a public and secret key spaces pkey and skey, together with a relation pkey_pair to tell which secret key correspond to which public key. We furthermore assume a symmetric key space key and an encrypted symmetric key space ekey together with distributions keyD and ekeyD on them. 8 Finally we also assume that we have a type of ciphers and a type of plaintexts together with a distinguished null plaintext (which we will write as 0), as well as a distribution on ciphers cipherD. In the original SSP paper [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF], these distributions are uniform distributions and these types are described using bit-strings but we decided for a more abstract approach, not only because it is slightly more general, but also because things appear simpler as we do not have to deal with low-level concerns. A KEM, 𝜂, is given by the following:

(1) 𝜂.kgen, a-state-preserving 9 and typically sampling-procedure which generates a valid public/secret key pair according to the pkey_pair relation; (2) 𝜂.encap, a state-preserving procedure which takes a public key pk and generates a symmetric key together with its asymmetric encryption with pk; (3) 𝜂.decap, a deterministic function-represented by a pure function in Coq-which returns a symmetric key from its encryption and the secret key. We additionally require that with an appropriate secret key, the original symmetric key can be recovered by applying 𝜂.decap to the encrypted key returned by 𝜂.encap. This specification, and the specification of 𝜂.kgen are handled in our formalization using the diagonal of our probabilistic relational program logic, i.e., we ensure that property 𝜑 holds of 𝑐 by verifying that the judgment

∀𝜓 . ⊨ { { {𝜓} } } 𝑐 ∼ 𝑐 { { {(𝑚 ′ 0 , 𝑎 0 ), (𝑚 ′ 1 , 𝑎 1 ). 𝜓 (𝑚 ′ 0 , 𝑚 ′ 1 ) ∧ 𝑎 0 = 𝑎 1 ∧ 𝜑 (𝑎 0 )} } } holds. A DEM,
𝜃 , is given by the following:

(1) 𝜃 .enc, a deterministic encryption function taking a symmetric key to turn a plaintext into a cipher; (2) 𝜃 .dec, a deterministic decryption function. Note that we do not need to know that 𝜃 .dec and 𝜃 .enc are inverses of each other to conduct the security proof so we do not require it. Of course, the DEM schemes of interest will verify this property as well.

For the remainder of this section, we assume that we are given a KEM 𝜂 and a DEM 𝜃 . Using them we define the KEM 𝑏 and DEM 𝑏 games in Figure 18 10 . These games are then used respectively as core keying and keyed games in the KEM-CCA 01 and DEM-CCA 01 game pairs (represented in Figure 19):

KEM-CCA 𝑏 = (KEM 𝑏 ∥ ID {Get} ) • KEY DEM-CCA 𝑏 = (ID {Gen} ∥ DEM 𝑏 ) • KEY
We finally combine 𝜂 and 𝜃 to form a public-key encryption (PKE) in the form the PKE-CCA 01 game pair defined in Figure 20 and Figure 22.

Security of the KEM-DEM construction

To state our PKE security theorem, we also define in Figure 21 and Figure 23 the MOD-CCA package which has the same exports as PKE-CCA 01 , but which will eventually be composed sequentially with 8 The same keyD is used in the KEY package. 9 Observationally, the state must be the same after execution of the procedure. 10 We abuse if notation here to match with our examples in §2. Formally, c being set in the two branches can be understood as the whole if computing the value that is then stored in c. KEM, DEM and KEY to form an auxiliary game, featured in Figure 24 and defined as: The security theorem that we formalize is then the following. Theorem 6.2. For every adversary to PKE-CCA 01 and AUX 01 A we have the following inequality:

AUX 𝑏 = MOD-CCA • (KEM 0 ∥ DEM 𝑏 ) • KEY.
𝛼 (PKE-CCA 01 ) (A) ≤ 𝛼 (KEM-CCA 01 ) (A • MOD-CCA • (ID export(KEM) ∥ DEM 0 )) + 𝛼 (DEM-CCA 01 ) (A • MOD-CCA • (KEM 1 ∥ ID export(DEM) )) + 𝛼 (KEM-CCA 01 ) (A • MOD-CCA • (ID export(KEM) ∥ DEM 1 ))
Note here that unfortunately, one detail of the proof leaks into the theorem statement: the adversary is also forbidden from using the state of the intermediary game pair AUX 01 . Concretely, that means an adversary is not allowed to use k_loc in addition to the locations of PKE-CCA 01 .

Proof of Theorem 6.2. We use Lemma 2.2 to establish the inequality

𝛼 (PKE-CCA 01 ) (A) ≤ 𝛼 (PKE-CCA 0 , MOD-CCA • (KEM 0 ∥ DEM 0 ) • KEY) (A) + 𝛼 (MOD-CCA • (KEM 0 ∥ DEM 0 ) • KEY, MOD-CCA • (KEM 0 ∥ DEM 1 ) • KEY) (A) + 𝛼 (MOD-CCA • (KEM 0 ∥ DEM 1 ) • KEY, PKE-CCA 1 ) (A) (6)
which corresponds to the following if we fold the definition of AUX:

𝛼 (PKE-CCA 01 ) (A) ≤ 𝛼 (PKE-CCA 0 , AUX 0 ) (A) + 𝛼 (MOD-CCA • (KEM 0 ∥ DEM 0 ) • KEY, MOD-CCA • (KEM 0 ∥ DEM 1 ) • KEY) (A) + 𝛼 (AUX 1 , PKE-CCA 1 ) (A) (7)
We then show that PKE-CCA 𝑏 and AUX 𝑏 are perfectly indistinguishable, using Theorem 2.4, i.e., we show they define equivalent procedures using an appropriate invariant. We detail the invariant and the code comparisons in Appendix A. We now proceed with rest of the proof of Theorem 6.2. Since PKE-CCA 𝑏 is perfectly indistinguishable from AUX 𝑏 , the inequality [START_REF] Almeida | The Last Mile: High-Assurance and High-Speed Cryptographic Implementations[END_REF] simplifies to

𝛼 (PKE-CCA 01 ) (A) ≤ 𝛼 (MOD-CCA • (KEM 0 ∥ DEM 0 ) • KEY, MOD-CCA • (KEM 0 ∥ DEM 1 ) • KEY) (A). (8)
Using Lemma 2.3 we replace the right-hand side to derive

𝛼 (PKE-CCA 01 ) (A) ≤ 𝛼 ((KEM 0 ∥ DEM 0 ) • KEY, (KEM 0 ∥ DEM 1 ) • KEY) (A • MOD-CCA). (9)
This (right-hand) upper bound corresponds to an instance of the left-hand side of the second inequality of Lemma 6.1 using A • MOD-CCA as distinguisher, meaning we have the inequality

𝛼 ((KEM 0 ∥ DEM 0 ) • KEY, (KEM 0 ∥ DEM 1 ) • KEY) (A • MOD-CCA) ≤ 𝛼 (KEM-CCA 01 ) (A • MOD-CCA • (ID export(KEM) ∥ DEM 0 )) + 𝛼 (DEM-CCA 01 ) (A • MOD-CCA • (KEM 1 ∥ ID export(DEM) )) + 𝛼 (KEM-CCA 01 ) (A • MOD-CCA • (ID export(KEM) ∥ DEM 1 )). (10)
We thus conclude using transitivity of ( 9) and [START_REF] Altenkirch | Monads need not be endofunctors[END_REF]. □

7 CASE STUDY: Σ-PROTOCOLS Σ-protocols form an important class of honest-verifier zero-knowledge protocols [START_REF] Damgaard | On Sigma-Protocols[END_REF][START_REF] Hazay | Efficient Secure Two-Party Protocols -Techniques and Constructions[END_REF]. A Σprotocol is defined on a relation R for which a prover, in zero-knowledge, can prove it knows a witness 𝑤 for a public statement ℎ such that the relations R ℎ 𝑤 holds.

In this section, we show how we can define the class of Σ-protocols in SSProve. This is not meant as an exhaustive treatment of Σ-protocols in SSP. We were mainly driven by comparison of SSProve to CryptHOL, in particular with the work of Butler et al. [START_REF] Butler | Formalising 𝛴-Protocols and Commitment Schemes Using CryptHOL[END_REF]. We prove the security of a transformation by converting a Σ-protocol in our class of protocols into a commitment scheme. A commitment scheme is a cryptographic primitive allowing anyone to publicly commit themselves to a value without revealing the value itself. Moreover, the party committing to the message can freely reveal the message at a later time with the guarantee that the value revealed is the value publicly committed to earlier.

Finally, we conclude the section by proving Schnorr's protocol [START_REF] Schnorr | Efficient signature generation by smart cards[END_REF] to be a member of the class of Σ-protocols and prove concrete security bounds. Schnorr's protocol allows a prover to convince a verifier that it knows the discrete logarithm of a group element. The general flow of a Σ-protocol can be seen in Figure 25. First, the prover uses the secret information 𝑤 to compute a message 𝑎 which is sent to the verifier. Second, the verifier samples a challenge 𝑒 uniformly at random from some challenge space and sends it to the prover. Third, the prover computes a response 𝑧 based on the secret information, the message, and the challenge. The response is then sent to the verifier. Finally, the verifier takes the public information, message, challenge, and response and checks whether it is convinced that the prover knows the secret.

The combination of the message, challenge, and response is commonly referred to as the transcript of the protocol.

We say that a Σ-protocol is secure when both of the following hold.

(1) There exists an efficient simulator which, given the public information and a fixed challenge, can produce a transcript that is indistinguishable from a real execution of the protocol with the same challenge. This is commonly referred to as the protocol being special honest-verifier zero-knowledge. (2) Given two accepting transcripts with the same initial message and different challenges, the witness for the relation can be reconstructed. This property is known as special soundness.

7.1 The SIGMA scheme Σ-protocols have been formalized before. Butler et al. [START_REF] Butler | Formalising 𝛴-Protocols and Commitment Schemes Using CryptHOL[END_REF] formalize a number of Σ-protocols in CryptHOL, and prove compositional properties of these protocols. Sidorenco et al. [START_REF] Sidorenco | Formal security analysis of MPC-in-the-head zeroknowledge protocols[END_REF] formalize Σ-protocols in EasyCrypt, and combine them with a formalization of multi-party computation (MPC) to formalize a, so-called, MPC-in-the-head protocol.

For our representation of Σ-protocols, we build on both these formalizations to define the SIGMA scheme and its corresponding security properties.

(1) Σ.Init, a non-deterministic procedure generating a message and state given access to the witness and public statement. (2) Σ.Response, a procedure generating a response from a state, witness, public statement, previous message, and any challenge. (3) Σ.Verify, a deterministic procedure returning a boolean based on all information sent in the protocol. (4) Σ.Simulate, a function computing a tuple (message, response) from a public statement and any challenge. (5) Σ.Extract, a procedure that given two transcripts either outputs a witness or fails. Additionally, we assume uniform distributions, 𝑐ℎ𝑎𝑙𝑙𝑒𝑛𝑔𝑒𝐷 and 𝑤𝑖𝑡𝑛𝑒𝑠𝑠𝐷, for sampling challenges and witnesses of the relation, respectively.

Security is defined as several games interacting utilizing the SIGMA scheme. The various security games are shown in Figure 26 and Figure 27 .

For any game which depends on a Σ scheme, we denote the scheme as follows: P 𝑆 denotes the P game depending on the Σ scheme 𝑆. For brevity, the scheme is sometimes omitted from the notation.

Definition 7.1. The special honest-verifier zero-knowledge security of an instantiation of a SIGMA scheme 𝑆 against adversary A is the advantage 𝛼 (SHVZK 0 𝑆 , SHVZK 1 𝑆 ) (A). Definition 7.2. The special soundness of an instantiation of a SIGMA scheme 𝑆 against adversary A is the advantage 𝛼 (SOUND 0 𝑆 , SOUND

Commitment Schemes from Σ-Protocols

A commitment scheme is another cryptographic primitive allowing a committer with some message 𝑚𝑠𝑔 to convince a verifier of two things: First, that 𝑚𝑠𝑔 has a fixed value set before contacting the verifier. Second, that the committer can at any later time reveal the value of 𝑚𝑠𝑔 to the verifier.

In particular, it must be the case that the verifier is convinced that the revealed message has not been changed from the original fixed message.

A commitment scheme is parameterized by types of messages, opening keys, and commitments. The scheme is given by the following:

(1) Commit, a probabilistic and stateful procedure, which produces a commitment from a message and an opening key. (2) Ver, which takes as input a commitment, message, and opening key and checks the validity of the commitment.

Definition 7.3. A commitment scheme is called secure when it is both hiding and binding:

• Hiding: For any commitment 𝑐 produced from message 𝑚𝑠𝑔 there exists a message 𝑚𝑠𝑔 ′ ≠ 𝑚𝑠𝑔 with commitment 𝑐 ′ indistinguishable from 𝑐. • Binding: For any commitment 𝑐 it is infeasible to find messages with opening keys (𝑚𝑠𝑔, 𝑜) and (𝑚𝑠𝑔 ′ , 𝑜 ′ ) with 𝑚𝑠𝑔 ≠ 𝑚𝑠𝑔 ′ such that both messages are valid openings for 𝑐.

For any given instance of a commitment scheme we define the security definitions from Definition 7.3 as the security games seen in Figure 30 and Figure 31.

Following the presentation of Damgaard [START_REF] Damgaard | On Sigma-Protocols[END_REF], we show how our SIGMA scheme with related security games can be used to construct a commitment scheme. This result is mostly of theoretical interest, and has previously been formalized in CryptHOL [START_REF] Butler | Formalising 𝛴-Protocols and Commitment Schemes Using CryptHOL[END_REF]. We formalize the result in SSProve to experiment with leveraging the package laws to build one protocol from another, and compare this result with the construction in CryptHOL in Section 7.2.1.

The key component of this transformation is the COM package shown in Figure 29. Here, COM is parameterized by the SIGMA scheme. Moreover, COM is meant to be composed with the KEY package, which is responsible for distributing the public and secret keys between the parties, and as such imports Init and Get. The KEY package is shown in Figure 28. Note that the KEY package contains the signing key. We use the KEY package because we need to sample a commitment key which fits the relation of the Σ-protocol without revealing the underlying witness used. Without this package (1) Commit, which uses the public and secret parts of the relation to produce a commitment to the challenge 𝑒. For this transformation, the commitment is the initial message of the underlying Σ-protocol. (2) Ver, which takes the commitment and the opening information and verifies their consistency. This, again, is dependent on the underlying Σ-protocol.

In this transformation, the types of the underlying Σ-protocol dictate the types of the commitment scheme. In particular, the message type of the commitment scheme is the type of the challenge used in the Σ-protocol.

First, in Theorem 7.4 we show that the construction is hiding with its security bounded by the Special Honest-Verifier Zero-Knowledge property of the underlying Σ-protocol. Theorem 7.4. For any instantiation of the SIGMA scheme, the commitment scheme given by COM•KEY, where the adversary is given oracle access to the KEY package, is hiding with the following advantage:

𝛼 ((HIDE 0 • COM • KEY) ∥ KEY, (HIDE 1 • COM • KEY) ∥ KEY) (A) ≤ 𝛼 ((HIDE 0 • AUX • SHVZK 0 ) ∥ KEY, (HIDE 1 • AUX • SHVZK 1 ) ∥ KEY) (A) + 𝛼 (SHVZK 01 ) (A • (HIDE 0 • AUX ∥ KEY)) + 𝛼 (SHVZK 01 ) (A • (HIDE 1 • AUX ∥ KEY))
where AUX is the package given by inlining (SIGMA ∥ KEY) into COM and replacing the call to the Σ-protocol simulator with SHVZK 1 .𝑀𝑎𝑖𝑛. Note that SHVZK 1 .𝑀𝑎𝑖𝑛 requires both a public statement and package: COM mem: The SHVZK 1 .𝑀𝑎𝑖𝑛 procedure is called with the statement and witness produced by KEY. 11 11 An anonymous reviewer points out that it should be possible to obtain a sharper bound as follows. The hiding games for a commitment scheme contains some redundancy: HIDE 0 is already a left-or-right security notion in itself, and is compared to the ideal HIDE 1 game which commits to random messages. This duplication appears in the advantage above as the SHVZK advantage counted twice, when once would be sufficient with a different formulation of the hiding games. We prefer to stick to the present presentation, as it facilitates comparison with the work of Butler et al. [START_REF] Butler | Formalising 𝛴-Protocols and Commitment Schemes Using CryptHOL[END_REF].

Commit (m): Init () h ← Get () (c , o) ← Σ. Simulate (h , m) return (c , o) Ver (c , m , o): h ← Get () v ← Σ. Verify (h , c , m , o) return v
Proof of Theorem 7.4. The HIDE package is introduced in Figure 30. First, let D = A • (ID 𝑒𝑥𝑝𝑜𝑟𝑡𝑠 (HIDE) ∥ KEY). Applying Lemma 2.2 we obtain:

𝛼 ((HIDE 0 • COM • KEY), (HIDE 1 • COM • KEY)) (D) ≤ 𝛼 ((HIDE 0 • COM • KEY), HIDE 0 • AUX • SHVZK 1 ) (D) + 𝛼 (HIDE 0 • AUX • SHVZK 1 , HIDE 0 • AUX • SHVZK 0 ) (D) + 𝛼 (HIDE 0 • AUX • SHVZK 0 , HIDE 1 • AUX • SHVZK 0 ) (D) + 𝛼 (HIDE 1 • AUX • SHVZK 0 , HIDE 1 • AUX • SHVZK 1 ) (D) + 𝛼 (HIDE 1 • AUX • SHVZK 1 , (HIDE 1 • COM • KEY)) (D)
The advantage of moving to and from the AUX package is 0, since AUX consists of COM where the KEY package inlined and the simulator is replaced with calls to the SHVZK package.

By Lemma 2.3:

𝛼 (HIDE 0 • AUX • SHVZK 1 , HIDE 0 • AUX • SHVZK 0 ) (D) = 𝛼 (SHVZK 1 , SHVZK 0 ) (D • HIDE 0 • AUX).
This gives us one of the bounds we are looking for. Similarly, the other SHVZK bound is obtained from 𝛼 (HIDE

1 • AUX • SHVZK 0 , HIDE 1 • AUX • SHVZK 1 ) (D).
This leaves us with 𝛼 (HIDE 0

• AUX • SHVZK 0 , HIDE 1 • AUX • SHVZK 0 ) (D)
, which is the last bound of Theorem 7.4. □

The binding property states that it must be infeasible for an adversary to produce two openings to the same commitments. Usually, this property is stated as: the probability of BIND • COM returning true, for any input, is sufficiently small. In SSProve, we do not have a unary logic to express such a statement. Rather, we prove in our relational logic that any adversary which makes BIND • COM return true, can be used to construct a program that outputs a witness of the relation. The package using the adversary to extract a witness for the relation is given by Figure 32. If a Σ-protocol is used to construct the commitment scheme, then the binding game is infeasible to win, because it is infeasible to compute the witness from the statement in a Σ-protocol. 12Theorem 7.5. For any instantiation of the Σ scheme, the probability of winning the binding game or computing the witness from the statement only differ by the probability of Σ.Extract outputting a valid witness for the relation:

𝛼 (BIND • (COM • KEY), BIND-Aux • SOUND 0 ) (A • (ID 𝑒𝑥𝑝𝑜𝑟𝑡𝑠 (BIND) ∥ KEY)) ≤ 𝛼 (SOUND) (A • ((BIND-AUX • KEY)) ∥ KEY).
To prove Theorem 7.5, we use Lemma 2.2 and Lemma 2.3 to replace the commitments with Σ-protocol transcripts, via SOUND 1 .

Comparison to Formalization in CryptHOL.

The construction deriving commitment schemes from Σ-protocols has also been formalized in CryptHOL [START_REF] Butler | Formalising 𝛴-Protocols and Commitment Schemes Using CryptHOL[END_REF]. In their definition, the commitment scheme construction is dependent on the types needed to instantiate a Σ-protocol. The proofs of hiding and binding are then quantified over any secure Σ-protocol that can be formed from the specified types. In particular, it is required that the distinguishing advantage on the special honest-verifier zero-knowledge security game is 0. Moreover, they assume that the Σ.Response and Σ.Verify procedures of the Σ-protocol terminate on all inputs.

In contrast, our security bounds defined in Theorem 7.4 and Theorem 7.5 make no assumptions on the underlying Σ-protocol other than that it implements the SIGMA interface. Because our results hold for any SIGMA package, we obtain a more general notion of security for the hiding property in Theorem 7.4, where the security bound is directly related to the security of the underlying Σ-protocol.

The imperfect game hops are justified by the package theorems of SSProve, which can be seen in the proof of Theorem 7.4. In particular, this allows us to accumulate the advantage from our game-hops into our final security bound, whatever the respective intermediate advantages may be.

Without the ability to reason about the advantage of composed packages, the proof would have had to involve significantly more steps, or make the same assumptions as in [START_REF] Butler | Formalising 𝛴-Protocols and Commitment Schemes Using CryptHOL[END_REF]. Namely, if we adopt the same assumption, then the proof of the security bounds can be done entirely within the relational logic itself. More concretely, the assumption of perfect special honest-verifier zeroknowledge reduces the statement from an adversary comparing both programs to the two programs being equivalent in the relation logic.

Concrete Implementation: Schnorr's protocol

The Schnorr protocol [START_REF] Schnorr | Efficient signature generation by smart cards[END_REF] is parameterized over a cyclic group (G, *) with 𝑞 elements generated by 𝑔. Schnorr's protocol is a Σ-protocol for the relation (ℎ, 𝑤) ∈ R ⇐⇒ ℎ = 𝑔 𝑤 , where 𝑤 is an element of Z 𝑞 and ℎ ∈ G.

Messages are elements 𝑎 ∈ G and responses are elements 𝑧 ∈ Z 𝑞 . Challenges are sampled from a uniform distribution over Z 𝑞 .

The protocol is implemented as an SSP package as shown in Figure 33. In particular, the package exports match the expected imports of our Σ-protocol security statements. Lemma 7.6 (Schnorr SHVZK). For any adversary A we have the following equality:

𝛼 (SHVZK 01 SCHNORR ) (A) = 0
Proof of Lemma 7.6. We use Theorem 2.4 to show the two packages are perfectly indistinguishable. After inlining the definition of Schnorr's protocol we get the code found in Table 1. Since the SHVZK 𝑏 package does not use state and the procedures of Σ scheme are stateless we use equality of heaps as our invariant. . We show this indeed holds:

• COM SCHNORR • KEY (HIDE 0 • COM SCHNORR • KEY).Hide(m1, m2) (HIDE 1 • COM SCHNORR • KEY).Hide(m1, m2) k <$ uniform bool Init () h ← Get () r <$ witnessD if k then a ← g r z ← r +
𝑔 𝑧 = 𝑎 • ℎ 𝑒 ∧ 𝑔 𝑧 ′ = 𝑎 • ℎ 𝑒 ′ ∧ 𝑒 ≠ 𝑒 ′ =⇒ ℎ = 𝑔 (𝑧-𝑧 ′ )/(𝑒 -𝑒 ′ ) = 𝑔 𝑤 ′ .

□

Based on Lemma 7.6 and Lemma 7.7 we can instantiate Theorem 7.4 and Theorem 7.5. For the latter, we can directly apply the theorem to show that any adversary has no advantage between the binding game and directly extracting the witness. For the former, the adversary also has no advantage, which we show in Theorem 7.8. Theorem 7.8. For all adversaries A we get the following equality for the commitment scheme instantiated from Schnorr's protocol:

𝛼 (HIDE 01 • COM SCHNORR • KEY) (A) = 0
Proof of Theorem 7.8. We use Theorem 7.4 to obtain:

𝛼 ((HIDE 0 • COM • KEY) ∥ KEY, (HIDE 1 • COM • KEY) ∥ KEY) (A) ≤ 𝛼 ((HIDE 0 • AUX • SHVZK 0 ) ∥ KEY, (HIDE 1 • AUX • SHVZK 1 ) ∥ KEY) (A) + 𝛼 (SHVZK) (A • (HIDE 0 • AUX ∥ KEY)) + 𝛼 (SHVZK) (A • (HIDE 1 • AUX ∥ KEY))
From Lemma 7.6 we get the two terms involving the advantage on the SHVZK game is 0.

𝛼 ((HIDE

0 • COM • KEY) ∥ KEY, (HIDE 1 • COM • KEY) ∥ KEY) (A) ≤ 𝛼 ((HIDE 0 • AUX • SHVZK 0 ) ∥ KEY, (HIDE 1 • AUX • SHVZK 1 ) ∥ KEY) (A)
To finish the proof we show that HIDE 0 • AUX • SHVZK 0 and HIDE 1 • AUX • SHVZK 0 are perfectly indistinguishable using Theorem 2.4. After inlining package composition and simplification of the if-statement we end up with the code comparison found in Table 3.

Because both sides use COM to store the value of e we cannot use equality of heaps as the invariant since the two sides store different values. Instead, we rely on the equality of heaps on all locations except the location of e. With the invariant fixed we now show equivalence between the two programs.

Looking at Table 3, we observe that the random sampling of e in the right-hand program has no counterpart on the left side. However, the particular choice of value for e on the right is not important: e simply gets used to compute z and gets stored in e_loc. We can thus remove the sampling by appealing to the sample-irrelevant rule. This transformation is possible since our invariant allows us to ignore the value of e stored in memory on both sides. We are then left with the two sides being equal barring the computation of the value 𝑧 and storing the value of 𝑧. Fortunately, the relational program logic supports one-sided rules for writing memory. With this we have the same program on both sides up to the return statement. Last, we can conclude perfect equivalence since the return values are equal and no memory operations altered any locations except the locations ignored by the invariant. □

We omit the simple proof of the binding property [42, pg.9], which can be found in our formalization (Lemma commitment_binding in SigmaProtocol.v).

RELATED WORK

SSProve is the first verification framework for SSP, yet the formal verification of cryptographic proofs in other styles has been intensely investigated [START_REF] Barbosa | SoK: Computer-aided cryptography[END_REF]. In this section we survey the closest related work in this space.

CertiCrypt [START_REF] Barthe | Formal certification of code-based cryptographic proofs[END_REF] is a foundational Coq framework for game-based cryptographic proofs. Cer-tiCrypt does not support modular proofs and is no longer maintained, yet it is seminal work that has inspired many other tools in this space, such as EasyCrypt, FCF, etc. The logic we introduce in §4 is also inspired by the probabilistic relational Hoare logic at the core of CertiCrypt. FCF [START_REF] Petcher | The Foundational Cryptography Framework[END_REF] is a more recent foundational Coq framework for cryptographic proofs that was used to verify the HMAC implementations in OpenSSL [START_REF] Beringer | Verified Correctness and Security of OpenSSL HMAC[END_REF] and mbedTLS [START_REF] Ye | Verified Correctness and Security of mbedTLS HMAC-DRBG[END_REF]. In contrast to CertiCrypt's (and EasyCrypt's) deep embedding of a probabilistic While language, FCF represents code with finite probabilities and non-termination using a monadic embedding, similar to the free monad we use for code in §3.1. The advantage of such an embedding is that code can be both easily manipulated as a syntactic object (e.g., to define package composition in §3.1) and easily lifted to a probability monad when needed ( §3.2 and §5.2), all without leaving Gallina, the internal language of Coq. This monadic representation of computational effects could also allow a more modular treatment of programs exhibiting effects of different nature such as communications with an external process [START_REF] Maillard | The next 700 relational program logics[END_REF]. Building a formalization of SSP on top of FCF may also be possible in principle though, and maybe even more interesting in practice could be rebasing SSProve on a simpler but less modular semantic model in the style of FCF or XHL [START_REF] Strub | XHL[END_REF] (as discussed in §5.5).

EasyCrypt [START_REF] Barthe | EasyCrypt: A Tutorial[END_REF][START_REF] Barthe | Computer-Aided Security Proofs for the Working Cryptographer[END_REF] is a proof assistant and verification tool specifically designed for gamebased cryptographic proofs and built from scratch. This state-of-the-art tool provides not only a probabilistic relational Hoare logic in the style of CertiCrypt (as we also do in section 4), but also a unary logic for reasoning about the probabilities of bad events [START_REF] Barthe | A Program Logic for Union Bounds[END_REF][START_REF] Barthe | Formal certification of code-based cryptographic proofs[END_REF] (which is, as mentioned in subsection 2.3, future work for SSProve). EasyCrypt has for instance been used to prove security of Amazon Web Services' Key Management Service [START_REF] Almeida | A Machine-Checked Proof of Security for AWS Key Management Service[END_REF]; of electronic voting schemes [START_REF] Constantin Catalin Dragan | Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co[END_REF]; of zeroknowledge protocols [START_REF] Firsov | Zero-Knowledge in EasyCrypt[END_REF]; of secure multiparty computation constructions [START_REF] Almeida | Machine-checked ZKP for NP relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head[END_REF]; of distance-bounding protocols [START_REF] Boureanu | Mechanised Models and Proofs for Distance-Bounding[END_REF]; and of low-level implementations of cryptographic primitives [START_REF] Almeida | Jasmin: High-Assurance and High-Speed Cryptography[END_REF][START_REF] Almeida | The Last Mile: High-Assurance and High-Speed Cryptographic Implementations[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][START_REF] Barthe | High-Assurance Cryptography in the Spectre Era[END_REF][START_REF] Basavesh | Enforcing Fine-grained Constant-time Policies[END_REF]]. EasyCrypt's good integration with automatic theorem provers (e.g., SMT solvers) seems helpful for such proofs, even if it does come at a cost in terms of trusted computing base. EasyCrypt also comes with an ML-style module system [START_REF] Barbosa | Mechanized Proofs of Adversarial Complexity and Application to Universal Composability[END_REF], as well as other abstraction mechanisms such as "theories". The default way of mechanizing proofs in EasyCrypt is, however, quite different than that of SSP. The EasyCrypt abstraction mechanisms were designed for allowing reuse of code and theorems [START_REF] Barthe | EasyCrypt: A Tutorial[END_REF], but they are rarely used at the moment to provide a modular high-level structure to cryptographic reduction proofs in the style of SSP [START_REF] Dupressoir | Bringing State-Separating Proofs to EasyCrypt -A Security Proof for Cryptobox[END_REF].

In concurrent work, Dupressoir et al. [START_REF] Dupressoir | Bringing State-Separating Proofs to EasyCrypt -A Security Proof for Cryptobox[END_REF] show that they can mechanize in EasyCrypt an SSPstyle multi-instance security proof for the Cryptobox [START_REF] Daniel | Cryptography in NaCl[END_REF] KEM-DEM [START_REF] Cramer | Design and Analysis of Practical Public-Key Encryption Schemes Secure against Adaptive Chosen Ciphertext Attack[END_REF] construction, and they discuss the various trade-offs they had to navigate and the strengths and shortcomings of EasyCrypt for formalizing such SSP-style proofs. Their multi-instance setting comes with specific challenges that do not appear in our mechanized proof from §6, such as the adversarial ability to create corrupt key instances. Yet despite the different setting, the high-level structure of the proofs seems similar to us.

Beyond this case study, we focus on providing a general framework for SSP proofs, including formal definitions of SSP packages, their composition, and the corresponding algebraic laws. Dupressoir et al. [START_REF] Dupressoir | Bringing State-Separating Proofs to EasyCrypt -A Security Proof for Cryptobox[END_REF] show instead informally, in the context of their example, how SSP concepts can be mapped to existing features in EasyCrypt. In particular, games are mapped to modules, and packages with imports are mapped to ML-style functors [START_REF] Milner | The Definition of Standard ML[END_REF], i.e., modules parameterized by other modules. Modules and functors are not fully first class in EasyCrypt though: while it is possible to quantify over modules, formulas cannot talk about module equality [START_REF] Stoughton | EasyCrypt Reference Manual[END_REF]. As a result, SSP-style laws cannot be stated or proven, and one has to manually write down all the functors involved in the proof, and argue about equality of the individual procedures instead.

SSP also has a notion of parameterized packages, in particular packages parameterized by crypto schemes or multi-instance packages [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF]Section 5]. For the former, in SSProve we can easily parametrize packages over parameters like crypto schemes using the expressive abstraction mechanisms of Coq's functional programming language, such as functions returning packages. Dupressoir et al. achieve something similar using the module-level abstraction mechanisms of EasyCrypt, choosing between functors and theories on a case by case basis [52, pg. 7]. The lattermulti-instance packages in SSP-are regular packages for which the names of the procedures (defined or used by the package) are indexed by natural numbers. To support multi-instance packages in SSProve a small technical change is needed: we can parametrize both the packages' memory locations and procedure names by an offset in order to make each instance distinct, which some of the authors have already tried out in ongoing work on formally connecting SSProve and Jasmin [START_REF] Almeida | Jasmin: High-Assurance and High-Speed Cryptography[END_REF][START_REF] Philipp | The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography[END_REF]. By contrast, Dupressoir et al. [START_REF] Dupressoir | Bringing State-Separating Proofs to EasyCrypt -A Security Proof for Cryptobox[END_REF] represent a multi-instance package as a single regular module (or functor) in EasyCrypt, having as state a map from instance indices to the actual state of each instance, and where the procedures also take an explicit instance index as argument.

SSProve gives the assert operation from SSP a simple and clearly defined semantics: assertion failure samples from the empty probability subdistribution (the same as entering an infinite loop in EasyCrypt). While this is not the only choice [START_REF] Bellare | Subtleties in the Definition of IND-CCA: When and How Should Challenge Decryption Be Disallowed?[END_REF], this formalizes our understanding of the following informal convention from the paper introducing SSP [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF]: "all our definitions and theorems apply only to code that never violates assertions. " By contrast, Dupressoir et al. [START_REF] Dupressoir | Bringing State-Separating Proofs to EasyCrypt -A Security Proof for Cryptobox[END_REF], manually encode a different, "oracle silencing" semantics for assertion failures [START_REF] Rogaway | Simplifying Game-Based Definitions -Indistinguishability up to Correctness and Its Application to Stateful AE[END_REF] in their case study, but without formally providing an assert construct, which seems non-trivial to formalize for their semantics.

SSProve faithfully follows the SSP model for memory initialization, allowing to express SSP proofs more naturally. Using default initial values for implicitly initializing all state variables allows us to define the notion of distinguishing advantage in terms of running on an initial memory, as done in SSP. By contrast, Dupressoir et al. [START_REF] Dupressoir | Bringing State-Separating Proofs to EasyCrypt -A Security Proof for Cryptobox[END_REF] use a mix of explicit initialization and logical preconditions to restrict the memories considered to those which are properly initialized. Finally, one aspect in which we took a similar design decision in SSProve to Dupressoir et al. [START_REF] Dupressoir | Bringing State-Separating Proofs to EasyCrypt -A Security Proof for Cryptobox[END_REF], is the absence of the implicit 𝛼-renaming conventions and pervasive state separation of Brzuska et al. [START_REF] Brzuska | State Separation for Code-Based Game-Playing Proofs[END_REF]. We instead reason about concrete locations and explicitly require state separation only between adversaries and the games with which they are composed. Reasoning about concrete locations in a shared global memory is not without downsides though, since as seen in §2.3 and §6.3 sometimes details of the proofs or assumptions do leak into the final theorem statements, so more research on better supporting private state for machine-checked modular cryptography would be helpful, in particular to also allow fresh locations to be allocated.

EasyUC [START_REF] Canetti | EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security[END_REF] aims to address the lack of composability in game-based proofs by formalizing the Universal Composability (UC) framework [START_REF] Canetti | Universally Composable Security[END_REF] using EasyCrypt. EasyUC replaces the interactive Turing machines in UC with EasyCrypt functions. It was used to prove a secure messaging protocol composed of Diffie-Hellman and one-time pad. More recent work develops a DSL [START_REF] Canetti | UC Domain Specific Language[END_REF] on top of EasyUC for hiding away the boilerplate needed to mediate between procedure-based communication in EasyCrypt and co-routine-based communication in the UC framework. Barbosa et al. [START_REF] Barbosa | Mechanized Proofs of Adversarial Complexity and Application to Universal Composability[END_REF] add automatic complexity analysis to EasyCrypt and use it for another formalization of UC. ILC [START_REF] Liao | ILC: a calculus for composable, computational cryptography[END_REF] is a process calculus modelling some of the key ideas behind the UC framework, in particular its co-routine based communication mechanism, while completely abstracting away from interactive Turing machines. ILC has not yet been formalized in a proof assistant. SSP was in part inspired by the UC framework, but focuses on making game-based proofs more modular and scalable, without targeting universal composability. A more precise comparison between SSP and UC proofs would be interesting, but out of scope for the current paper. Recent work by Brzuska and Oechsner [START_REF] Brzuska | A State-Separating Proof for Yao's Garbling Scheme[END_REF] and Brzuska et al. [START_REF] Brzuska | Key-schedule Security for the TLS 1.3 Standard[END_REF] indicates that SSP can also be relevant for simulation-based security.

CryptHOL [START_REF] Basin | CryptHOL: Game-Based Proofs in Higher-Order Logic[END_REF] is a foundational framework for game-based proofs that established a connection between relational parametricity and coupling, the main workhorse of pRHL, to achieve automation in the Isabelle/HOL proof assistant. CryptHOL also makes use of the extensive mathematical libraries of Isabelle/HOL. More proof engineering and automation would be needed for SSProve to have a chance at matching the elegance of CryptHOL's formalization of ElGamal or PRF-based encryption. CryptHOL [START_REF] Lochbihler | Formalizing Constructive Cryptography using CryptHOL[END_REF] has been also used to formalize Constructive Cryptography [START_REF] Maurer | Constructive Cryptography -A New Paradigm for Security Definitions and Proofs[END_REF] (an instance of Abstract Cryptography [START_REF] Maurer | Abstract Cryptography[END_REF]), another composable framework that inspired SSP, and the example of a one-time pad. CryptHOL converters are similar to SSP packages, however, there are certain distinctions that we discuss here: To begin, converters combine all their procedures into a single resumption-like value, resulting in simpler interfaces consisting of a dependent pair (𝐴, 𝐵), where 𝐴 denotes a global input type and 𝐵 a global output type of the bundled procedures, and an additional invariant is maintained to ensure that outputs correspond to specific inputs. Procedures in SSP packages are written using a free monad that captures the probabilistic operations without evaluating them, and only at a later stage these operations are interpreted, whereas converters are built directly over the probabilistic subdistributions monad. Similarly, SSP packages utilize uninterpreted operations for stateful operations, whereas converters keep a hidden state using the coinductive structure of resumptions. CryptHOL provides a bisimilarity notion that can be used to prove perfect indistinguishability, similar to our Theorem 2.4, but in addition, they also provide a bisimulation-style proof rule for establishing trace equivalence, which as they show is needed in certain cryptographic arguments.

Regarding automation, both Isabelle/CryptHOL and EasyCrypt are based on classical HOL and provide powerful SMT-based automation. A detailed comparison between the HOL-systems and systems like Coq based on dependent type theory is out of scope for the present paper. We merely observe that huge formalizations have been carried out in both traditions. On the narrow topic of SMT-based automation, we mention this is also being developed for Coq [START_REF] Armand | A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses[END_REF][START_REF] Czajka | Hammer for Coq: Automation for Dependent Type Theory[END_REF], and any progress on those projects could also profit SSProve. Another key part of the automation in EasyCrypt is the auto tactic, which tries a to apply rules of the program logic based on the structure of the code. We have a similar tactic in SSProve, which moreover, is easily extensible due to Coq's tactic language.

IPDL [START_REF] Gancher | A Core Calculus for Equational Proofs of Cryptographic Protocols[END_REF] is another recent Coq framework for cryptographic proofs. Although their motivation is similar to SSP and their interaction sets are reminiscent of packages, the relation of IPDL to other composable frameworks has not been worked out, and is out of scope for the current paper. Their compositional formalism seems closer to Constructive Cryptography [START_REF] Maurer | Constructive Cryptography -A New Paradigm for Security Definitions and Proofs[END_REF] than to UC. Another recent work that seems related to Constructive Cryptography is categorical composable cryptography [START_REF] Broadbent | Categorical composable cryptography[END_REF], which gives an abstract model of composable cryptographic security definitions in terms of categorically formulated resource theories [START_REF] Coecke | A mathematical theory of resources[END_REF]. The authors leave open the precise relation to Constructive Cryptography, or to other established cryptographic frameworks.

Computational Indistinguishability Logic (CIL) [START_REF] Barthe | Computational indistinguishability logic[END_REF] is another formal framework for reasoning about cryptographic primitives in terms of "oracle systems", which are inspired by probabilistic process algebra and which seem related to SSP packages. The operational model and the soundness of CIL have been formalized in Coq [START_REF] Corbineau | Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience[END_REF].

SSP packages have been motivated by ML modules [START_REF] Rossberg | F-ing modules[END_REF] and sequential composition of packages is similar to the usual composition of modules. No specific theory for probabilistic programming languages with stateful modules seems to be available, but Sterling and Harper [START_REF] Sterling | Logical relations as types: Proof-relevant parametricity for program modules[END_REF] provide a general module system. It would be interesting to specialize it to probabilistic stateful programs and compare it to packages.

FUTURE WORK

The high-level proofs done on paper in the miTLS project [START_REF] Bhargavan | Implementing and Proving the TLS 1.3 Record Layer[END_REF][START_REF] Bhargavan | Proving the TLS Handshake Secure (As It Is)[END_REF][START_REF] Brzuska | Key-schedule Security for the TLS 1.3 Standard[END_REF][START_REF] Fournet | Modular code-based cryptographic verification[END_REF] were the main inspiration for the SSP methodology and it would be an interesting challenge to scale SSProve to mechanizing such large security proofs in the future. This would for a start require more work on proof engineering and automation, as well as implementing a unary logic for reasoning about the probabilities of bad events [START_REF] Barthe | A Program Logic for Union Bounds[END_REF][START_REF] Barthe | Formal certification of code-based cryptographic proofs[END_REF]. The problem of verifying such large proofs all the way down to low-level efficient executable code is even more challenging, also given the large scale of a complete implementation for a protocol like TLS. Achieving this in Coq would probably require integrating with projects such as Jasmin [START_REF] Almeida | Jasmin: High-Assurance and High-Speed Cryptography[END_REF][START_REF] Almeida | The Last Mile: High-Assurance and High-Speed Cryptographic Implementations[END_REF], VST [START_REF] Appel | Verified Software Toolchain -(Invited Talk)[END_REF], or FiatCrypto [START_REF] Erbsen | Simple High-Level Code for Cryptographic Arithmetic -With Proofs, Without Compromises[END_REF]. Some of the authors have in fact been working on integrating SSProve with Jasmin [START_REF] Almeida | Jasmin: High-Assurance and High-Speed Cryptography[END_REF][START_REF] Almeida | The Last Mile: High-Assurance and High-Speed Cryptographic Implementations[END_REF] by defining a translation from the Coq representation of Jasmin programs to SSProve programs, while provably preserving semantics [START_REF] Philipp | The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography[END_REF]. This allows them to formally connect in Coq security proofs in SSProve to the assembly code produced by the Jasmin verified compiler.

An alternative would be to port SSProve to F ★ [START_REF] Swamy | Dependent Types and Multi-Monadic Effects in F*[END_REF], where at least functional correctness can be verified at that scale. Still many challenges would remain, including extending F ★ to probabilistic verification, giving F ★ modules first-class status, and extending the SSP methodology to support type abstraction and procedures with specifications. An interesting step in this direction is the preliminary work of Kohbrok et al. [START_REF] Kohbrok | Relational F* for State Separating Cryptographic Proofs[END_REF], who have implemented vanilla SSP packages in F ★ and attempted to automate state-separating proofs based on a library for partial setoids.

Finally, our formalization of Σ-protocols has been used recently to prove the security of the OpenVoteNetwork smart contract [START_REF] Sidorenco | A formal security analysis of Blockchain voting[END_REF].

1 Fig. 2 .

 12 Fig. 1. Package 𝑃

Fig. 3 .

 3 Fig. 3. Graphical representation of packages

Fig. 4 .Fig. 5 .

 45 Fig. 4. Packages PRF 0 and PRF 1

Fig. 6 .

 6 Fig. 6. Packages IND-CPA 0 and IND-CPA 1

Fig. 8 .

 8 Fig. 8. Enc procedures expanded

  mem : k_loc : option key Get () : k ← get k_loc assert (k ≠ ⊥) as kSome return ( getSome k kSome )

x

  ← c 1 ; c 2 := bind c 1 (λx.c 2 ) x ← p(a) ; c := call p a (λx.c) x ← get ℓ ; c := get ℓ (λx.c) put ℓ := v ; c := put ℓ v c x <$ D ; c := sample D (λx.c) assert e as H ; c := assertD e (λH.c)

3. 3 Fig. 13 .

 313 Fig. 13. Package MOD-CPA (repeated)

Definition 5 . 1 (

 51 Relative monad). Given a functor 𝐽 : I → C, a monad relative to 𝐽 (or 𝐽 -relative monad) is a functor 𝑀 : I → C equipped with "𝐽 -shifted" return and bind operations return : ∀(𝑋 : I). C(𝐽𝑋, 𝑀𝑋 ) bind : ∀(𝑋 𝑌 : I). C(𝐽𝑋, 𝑀𝑌 ) → C(𝑀𝑋, 𝑀𝑌 ) satisfying 𝐽 -shifted versions of the return and bind monad laws: bind 𝑋 ,𝑋 (return 𝑋 ) = id 𝑀𝑋 bind 𝑋 ,𝑌 (𝑘) • return 𝑋 = 𝑘 bind 𝑋 ,𝑍 (bind 𝑌 ,𝑍 (𝑙) • 𝑘) = bind 𝑌 ,𝑍 (𝑙) • bind 𝑋 ,𝑌 (𝑘)

Definition 5 . 2 (Definition 5 . 3 (

 5253 Left 𝐽 -relative adjunction). Consider functors 𝐽, 𝐿, 𝑅 in the following configuration 𝐿 and 𝑅 are 𝐽 -relative left and right adjoints respectively (𝐿 𝐽 ⊣ 𝑅) if there exists a natural isomorphism ∀(𝑋 : I) (𝑌 : C). D (𝐿𝑋, 𝑌 ) C(𝐽𝑋, 𝑅𝑌 ). In that case, the composition 𝑅𝐿 turns out to be a 𝐽 -relative monad and is said to be induced by the left relative adjunction 𝐿 𝐽 ⊣ 𝑅. Kleisli adjunction of a relative monad). Let 𝑀 : I → C be a 𝐽 -relative monad. We define its Kleisli category Kl(𝑀) to have • as objects, the objects of I.• as morphisms, Kl(𝑀) (𝑋, 𝑌 ) := C(𝐽𝑋, 𝑀𝑌 ).

Fig. 15 .

 15 Fig. 14. KEY package

Fig. 16 .Fig. 17 .

 1617 Fig. 16. Keying and keyed games combined

Fig. 18 .Fig. 19 .

 1819 Fig. 18. KEM 𝑏 and DEM 𝑏 games

Fig. 22 .Fig. 23 .Fig. 24 .

 222324 Fig. 22. PKE-CCA 𝑏 game graphically

Fig. 25 .

 25 Fig. 25. Σ-Protocol overview

Fig. 28 .

 28 Fig. 28. KEY package

Fig. 29 .Fig. 30 .Fig. 31 .Fig. 32 .

 29303132 Fig. 29. COM package

Fig. 33 .

 33 Fig. 33. SCHNORR Σ-scheme

  m1 * w put e_loc := Some m1 else a ← g r z ← r + m2 * w put e_loc := Some m1 put z_loc := Some z return a Init () h ← Get () m <$ challengeD a ← g r z ← r + m * w put e_loc := Some m put z_loc := Some z return a programs are indistinguishable if ℎ = 𝑔 𝑤 ′

  Fig. 7. Packages MOD-CPA 𝑏 import Eval from PRF 𝑖 Brzuska et al. [40] use a sequence of game-hops to bound 𝛼 (IND-CPA 01

	package: MOD-CPA 0				package: MOD-CPA 1
	mem:					mem:
	Enc ( msg ) :				Enc ( msg ):
	r <$ uniform {0, 1} 𝑛			msg ' <$ uniform {0, 1} 𝑛
	pad ← Eval ( r )				r <$ uniform {0, 1} 𝑛
	c ← msg xor pad				pad ← Eval (r )
	return (r , c )				c ← msg ' xor pad
						return (r , c)
	Enc	MOD-CPA	b	Eval	PRF	i

Packages CPA 0 and CPA 1 in ElGamal

  would have likely also exposed this flaw.

	package: DDH 0	package: DDH 1
	mem: pk : option pubKey	mem: pk : option pubKey
	sk : option secKey	sk : option secKey
	Query ()	Query ()
	sk <$ uniform {0 , ... , n -1}	sk <$ uniform {0 , ... , n -1}
	rnd <$ uniform {0 , ... , n -1}	rnd <$ uniform {0 , ... , n -1}
	pk ← g sk	rnd ' <$ uniform {0 , ... , n -1}
	return ( g sk ,g rnd ,g sk•rnd )	pk ← g sk
		return ( g sk ,g rnd ,g rnd' )
	Fig. 10. The DDH assumption states that DDH 0 and DDH 1 are computationally indistinguishable
	package: CPA 0	package: CPA 1
	mem: pk : option pubKey	mem: pk : option pubKey
	sk : option secKey	sk : option secKey
	counter : nat	counter : nat
	Get_pk () :	Get_pk () :
	return pk	return pk
	Challenge ( msg ) :	Challenge ( msg ):
	assert counter = 0	assert counter = 0
	( pk , sk ) ← KeyGen ()	(pk , sk ) ← KeyGen ()
	( c rnd , c msg ) ← Enc (pk , msg )	(c rnd , c msg ) <$ uniform G × G
	counter ++	counter ++
	return ( c rnd , c msg )	return (c rnd , c msg )
	Fig. 11.

Table 1 .

 1 Code comparison of SHVZK 0 and SHVZK 1 with Schnorr's protocol

Table 3 .

 3 Code comparison of HIDE 0 • COM SCHNORR • KEY and HIDE 1

In SSProve the procedure names within interfaces are also associated with argument and result types, but we omit this detail until §3.1.

We will still use the 𝜆 notation for programs.

Here we omit quantifications in pre-and postconditions for conciseness.

In a previous version of this work[START_REF] Abate | SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq[END_REF] we were -erroneously -not providing Get_pk() to the adversary, so the result

This type of raw code comes equipped with an induction principle (basically structural induction on trees), which is used for instance in the proof of Theorem 2.4, in Theorem 4.1, and in the definition of the bind operation and sequential composition of packages by recursion over code.

Here we write mem(𝑃 ) to denote the memory footprint of package 𝑃 . In the Coq formalization, we instead use a relation on a package and a set of memory locations stating that the packages only uses memory locations in the set but not necessarily all of them. This is a technical detail and in the remainder of the paper we will stick to the mem as a function notation.

Our definition of the binding game is equivalent to those used in other formalizations of commitment schemes[START_REF] Butler | Formalising 𝛴-Protocols and Commitment Schemes Using CryptHOL[END_REF][START_REF] Metere | Automated Cryptographic Analysis of the Pedersen Commitment Scheme[END_REF].An anonymous reviewer suggests that these definitions are reminiscent of a trapdoor commitment scheme. We leave a detailed comparison to future work.

ACKNOWLEDGMENTS

We are grateful to Arthur Azevedo de Amorim for his technical support and to Théo Laurent, Sabine Oechsner, and Ramkumar Ramachandra for participating in stimulating discussions. We are also grateful to Markulf Kohlweiss for pointing out a bug in our modelling of public-key encryption schemes in the ElGamal example, which we quickly fixed as discussed in §2.4. We also thank Brzuska et al. for their prompt fix of the informal proof of security for KEM-DEM [40] which allowed us to complete our formalization. Finally we are also very grateful to the anonymous reviewers of CSF and TOPLAS for their detailed and helpful feedback. This work was in part supported by

When comparing the code in Table 1 the programs immediately differ in the use of their randomly sampled values. To make the programs agree on return values we use the uniform rule from §4.1. First, we see that both sides assert that the relation R holds. We remove both asserts and assume for the rest of the proof that R holds. Applying uniform with 𝑓 : 𝑥 ↦ → 𝑥 + 𝑒 • 𝑤 and moving all constants into the return statement we obtain: (ℎ, 𝑔 𝑟 , 𝑒, 𝑟 + 𝑒 • 𝑤) ? = (ℎ, 𝑔 𝑓 (𝑧 ) • ℎ -𝑒 , 𝑒, 𝑓 (𝑟 )). We solve the goal with the following equality:

where we use the fact that the relation ℎ = 𝑔 𝑤 holds for our particular values of ℎ and 𝑤. □ Lemma 7.7 (Schnorr Special-Soundness). For all adversaries A we have the following equality:

Proof of Lemma 7.7. We use Theorem 2.4 to show the two packages are perfectly indistinguishable. After inlining the definition of Schnorr's protocol we get the code found in Table 2. Since neither Schnorr's protocol nor the SOUND 𝑏 package use state, we can use equality of heaps as our invariant.Both sides are given the same inputs so the two programs are indistinguishable after the two verifications. The if-statement in SOUND 0 is equal to the return value of SOUND 1 . Hence, the two

A PACKAGE EQUIVALENCE FOR KEM-DEM

In order to prove Theorem 6.2, we show that PKE-CCA 𝑏 and AUX 𝑏 (note that, as in §6, we assume we are given a KEM 𝜂 and a DEM 𝜃 corresponding to the ones used in both games) are perfectly indistinguishable using Theorem 2.4. After inlining package composition we end up with the code comparison found in Table 4, Table 5, and Table 6. We deliberately add extra newlines to align similar lines of code.

Because only AUX 𝑏 makes use of the KEY package, the k_loc memory location is only used on one side which means that we cannot use equality of heaps as an invariant. Instead, our invariant corresponds to ensuring the following three points:

(1) equality of heaps on all locations except k_loc;

(2) pk_loc will store ⊥ if and only if sk_loc stores ⊥;

(3) whenever k_loc and ek_loc are set-i.e., do not contain ⊥-in AUX 𝑏 , ek_loc will in fact contain the result of the encapsulation of the value stored in k_loc.

To preserve this last invariant we exploit the correctness of the KEM, as we will see later.

We will now address the equivalences corresponding to the three different procedures in the common export interface of PKE-CCA 𝑏 and AUX 𝑏 .

Equivalence for Pkgen. When looking at Table 4, we can see that the only difference is in the first two lines of AUX 𝑏 which are absent from PKE-CCA 𝑏 . Taken in isolation, they would break the equivalence because of the assert. Here we can leverage the invariant stating that the locations pk_loc and sk_loc are always mutually set, so that if sk_loc contains ⊥ then pk_loc does too. To exploit the invariant, we first swap commands on the right-hand side to perform the read of sk on both sides and we recover the fact that it must be ⊥. We also verify that the invariant is preserved as pk_loc and sk_loc are both set at the end of the run. Equivalence for Pkenc. In Table 5 we can see a lot of repetition and locations that are read at different occasions on the left-and right-hand sides. Thankfully our relational program logic supports one-sided rules for memory reads and writes that remember values that have been written and read; they correspond to rules like get-lhs or put-lhs that are presented at the end of §4.1. With this we have the same programs on both sides up to the following line:

To progress, we cannot merely use a simple application of the bind rule because we would then lose the information that k and ek are related. Instead, we use the specification of 𝜂 (the KEM) to get as a precondition, for the rest of the comparison, the fact that ek is the encryption of k. After that, on the right-hand side we make use of the invariant relating pk, k_loc, and ek_loc to ascertain that since ek_loc contains ⊥, so must k_loc. When the value of k_loc is read again on the right-hand side, we proceed as above to remember the value that was just stored. The rest of the proof is straightforward, we only have to show that we preserved the invariant when overwriting the memory, which means that we must show that the newly stored values in k_loc and ek_loc must indeed correspond to a pair of a key and its encryption, a fact that we recovered above.

Equivalence for Pkdec. For the most part before the if in Table 6, the equivalence proof is conducted in roughly the same way as above. Then we proceed with a case-analysis on ek = Some ek'. In the else branch, all of the asserts hold, as they hold in the lines above and the invariant stating that pk_loc is ⊥ if and only if sk_loc is satisfied, and furthermore the case-analysis yielded ek ≠ Some ek'. The rest of the code in the else branch then goes on to produce exactly the same result as the left-hand side.

The more interesting bit happens in the then branch where there is no call to the decapsulation procedure 𝜂.decap of the KEM. Instead, we exploit the invariant that states that the stored encrypted key in ek_loc corresponds to the encryption of the key in k_loc using the public key in pk_loc, a fact which we encoded by saying that in this case k is equal to 𝜂.encap(sk, ek). We conclude remembering that we are in the branch where ek = Some ek'. Now that the three procedures have been shown equivalent, we know that the two packages are indeed perfectly indistinguishable.