# CryptoVerif: a Computationally-Sound Security Protocol Verifier

Bruno Blanchet, Charlie Jacomme

► To cite this version:

Bruno Blanchet, Charlie Jacomme. CryptoVerif: a Computationally-Sound Security Protocol Verifier. RR-9526, Inria. 2023, pp.194. hal-04253820

HAL Id: hal-04253820

https://inria.hal.science/hal-04253820v1

Submitted on 23 Oct 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
Ínria

# CryptoVerif: a
Computationally-Sound
Security Protocol Verifier

Bruno Blanchet, Charlie Jacomme

## RESEARCH
## REPORT

Nº 9526

October 2023

Project-Team Prosecco
<figure><img src="image_2.png" /></figure>
<figure><img src="image_3.png" /></figure>

# CryptoVerif: a Computationally-Sound
Security Protocol Verifier

Bruno Blanchet*, Charlie Jacomme*

Project-Team Prosecco

Research Report n° 9526 — October 2023 — 194 pages

**Abstract:** This document presents the security protocol verifier CryptoVerif. CryptoVerif does not rely on the symbolic, Dolev-Yao model, but on the computational model. It can verify secrecy, correspondence properties (which include authentication), and indistinguishability properties. It produces proofs presented as sequences of games, like those manually written by cryptographers; these games are formalized in a probabilistic process calculus. CryptoVerif provides a generic method for specifying security properties of the cryptographic primitives. It produces proofs valid for any number of sessions of the protocol, and provides an upper bound on the probability of success of an attack against the protocol as a function of the probability of breaking each primitive and of the number of sessions. CryptoVerif is post-quantum sound: when the used cryptographic assumptions are valid for quantum adversaries, the proofs hold for quantum adversaries. It can work automatically, or the user can guide it with manual proof indications.

**Key-words:** security protocols, verification, computational model

RESEARCH CENTRE
PARIS

2 rue Simone Iff - CS 42112
75589 Paris Cedex 12

<footnote>* Inria</footnote>
CryptoVerif: un vérificateur de protocoles cryptographiques sûr dans le modèle calculatoire

**Résumé** : Ce document présente le vérificateur de protocoles cryptographiques CryptoVerif. CryptoVerif ne s'appuie pas sur le modèle symbolique de Dolev-Yao, mais sur le modèle calculatoire. Il peut vérifier le secret, les correspondances (qui comprennent l'authentification) et les propriétés d'indistinguabilité. Il produit des preuves par suites de jeux, comme celles écrites manuellement par les cryptographes ; ces jeux sont formalisés dans un calcul de processus probabiliste. CryptoVerif fournit une méthode générique pour spécifier les propriétés de sécurité des primitives cryptographiques. Il produit des preuves valables pour un nombre quelconque de sessions du protocole, et fournit une borne supérieure sur la probabilité de succès d'une attaque contre le protocole en fonction de la probabilité de casser chaque primitive et du nombre de sessions. CryptoVerif est sûr contre des attaquants quantiques : quand les hypothèses cryptographiques utilisées sont valides pour des attaquants quantiques, les preuves produites sont valides pour des attaquants quantiques. Il peut fonctionner automatiquement, ou l'utilisateur peut guider la preuve manuellement.

**Mots-clés** : protocoles cryptographiques, vérification, modèle calculatoire
# Contents

<table><tr><td>1</td><td>Introduction</td><td>5</td></tr><tr><td>2</td><td>A Calculus for Cryptographic Games</td><td>8</td></tr><tr><td>2.1</td><td>Syntax and Informal Semantics</td><td>8</td></tr><tr><td>2.2</td><td>Example</td><td>17</td></tr><tr><td>2.3</td><td>Type System</td><td>20</td></tr><tr><td>2.4</td><td>Formal Semantics</td><td>25</td></tr><tr><td>2.4.1</td><td>Definition of the Semantics</td><td>25</td></tr><tr><td>2.4.2</td><td>Properties</td><td>35</td></tr><tr><td>2.4.3</td><td>Each Variable is Defined at Most Once</td><td>44</td></tr><tr><td>2.4.4</td><td>Each Oracle is defined at most once</td><td>47</td></tr><tr><td>2.4.5</td><td>Variables are Defined Before Being Used</td><td>48</td></tr><tr><td>2.4.6</td><td>Typing</td><td>50</td></tr><tr><td>2.5</td><td>Subset for the Initial Game</td><td>51</td></tr><tr><td>2.6</td><td>Input Language with Channels instead of Oracles</td><td>53</td></tr><tr><td>2.6.1</td><td>Input Language Description</td><td>53</td></tr><tr><td>2.6.2</td><td>Translating from the Channel Calculus to the Oracle Calculus</td><td>54</td></tr><tr><td>2.7</td><td>Subsets used inside the Sequence of Games</td><td>56</td></tr><tr><td>2.8</td><td>Security Properties, Indistinguishability</td><td>58</td></tr><tr><td>2.8.1</td><td>Secrecy</td><td>66</td></tr><tr><td>2.8.2</td><td>Secrecy for a Bit</td><td>69</td></tr><tr><td>2.8.3</td><td>Correspondences</td><td>73</td></tr><tr><td>2.8.4</td><td>Computation of Advantages</td><td>79</td></tr><tr><td>2.8.5</td><td>Proof of Indistinguishability</td><td>88</td></tr><tr><td>2.8.6</td><td>Proof of queryequiv</td><td>89</td></tr><tr><td>3</td><td>Collecting True Facts</td><td>92</td></tr><tr><td>3.1</td><td>User-defined Rewrite Rules</td><td>96</td></tr><tr><td>3.2</td><td>Collecting True Facts from a Game</td><td>97</td></tr><tr><td>3.3</td><td>Local Dependency Analysis</td><td>102</td></tr><tr><td>3.4</td><td>Equational Prover</td><td>105</td></tr><tr><td>4</td><td>success: Criteria for Proving Security Properties</td><td>108</td></tr><tr><td>4.1</td><td>Secrecy</td><td>109</td></tr><tr><td>4.2</td><td>Correspondences</td><td>120</td></tr><tr><td>4.2.1</td><td>Example</td><td>120</td></tr><tr><td>4.2.2</td><td>Non-unique Events</td><td>123</td></tr><tr><td>4.2.3</td><td>Non-injective Correspondences</td><td>123</td></tr><tr><td>4.2.4</td><td>Injective Correspondences</td><td>128</td></tr><tr><td>5</td><td>Game Transformations</td><td>135</td></tr><tr><td>5.1</td><td>Syntactic Game Transformations</td><td>135</td></tr><tr><td>5.1.1</td><td>auto_SArename</td><td>135</td></tr><tr><td>5.1.2</td><td>expand_tables</td><td>136</td></tr><tr><td>5.1.3</td><td>expand</td><td>136</td></tr><tr><td>5.1.4</td><td>prove_unique</td><td>137</td></tr><tr><td>5.1.5</td><td>remove_assign</td><td>137</td></tr><tr><td>5.1.6</td><td>use_variable</td><td>138</td></tr></table>
<table><tbody><tr><td>5.1.7</td><td><strong>SArename</strong></td><td>139</td></tr><tr><td>5.1.8</td><td><strong>move</strong></td><td>140</td></tr><tr><td>5.1.9</td><td><strong>move array</strong></td><td>141</td></tr><tr><td>5.1.10</td><td><strong>move up</strong></td><td>141</td></tr><tr><td>5.1.11</td><td><strong>move if fun</strong></td><td>143</td></tr><tr><td>5.1.12</td><td><strong>insert_event</strong></td><td>144</td></tr><tr><td>5.1.13</td><td><strong>insert</strong></td><td>144</td></tr><tr><td>5.1.14</td><td><strong>replace</strong></td><td>144</td></tr><tr><td>5.1.15</td><td><strong>merge branches</strong></td><td>145</td></tr><tr><td>5.1.16</td><td><strong>merge arrays</strong></td><td>146</td></tr><tr><td>5.1.17</td><td><strong>guess i</strong></td><td>147</td></tr><tr><td>5.1.18</td><td><strong>guess x[c<sub>1</sub>,...,c<sub>m</sub>]</strong></td><td>156</td></tr><tr><td>5.1.19</td><td><strong>guess branch</strong></td><td>159</td></tr><tr><td>5.1.20</td><td><strong>global dep anal</strong></td><td>161</td></tr><tr><td>5.1.21</td><td><strong>simplify</strong></td><td>163</td></tr><tr><td>5.1.22</td><td><strong>all simplify</strong></td><td>167</td></tr><tr><td>5.1.23</td><td><strong>success simplify</strong></td><td>167</td></tr><tr><td>5.2</td><td><strong>crypto: Applying the Security Assumptions on Primitives</strong></td><td>175</td></tr><tr><td>5.2.1</td><td><strong>Basic Transformation</strong></td><td>175</td></tr><tr><td>5.2.2</td><td><strong>Optimizations for transf<sub>&phi;</sub>(FB)</strong></td><td>184</td></tr><tr><td>5.2.3</td><td><strong>Guiding the Application of Equivalences</strong></td><td>184</td></tr><tr><td>5.2.4</td><td><strong>Relaxing Hypothesis H6</strong></td><td>185</td></tr><tr><td>5.2.5</td><td><strong>Relaxing Hypothesis H'2</strong></td><td>185</td></tr><tr><td>5.2.6</td><td><strong>Soundness and Example</strong></td><td>186</td></tr><tr><td><strong>6</strong></td><td><strong>Proof Strategy</strong></td><td><strong>187</strong></td></tr><tr><td><strong>7</strong></td><td><strong>Conclusion</strong></td><td><strong>188</strong></td></tr></tbody></table>
# 1 Introduction

There exist two main approaches for analyzing security protocols. In the computational model, messages are bitstrings, and the adversary is a probabilistic polynomial-time Turing machine. This model is close to the real execution of protocols, but the proofs are usually manual and informal. In contrast, in the symbolic, Dolev-Yao model, cryptographic primitives are considered as perfect blackboxes, modeled by function symbols in an algebra of terms, possibly with equations. The adversary can compute using only these blackboxes. This abstract model makes it easier to build automatic verification tools, but the security proofs are in general not sound with respect to the computational model.

In contrast to most previous protocol verifiers, CryptoVerif works directly in the computational model, without considering the Dolev-Yao model. It produces proofs valid for any number of sessions of the protocol, in the presence of an active adversary. These proofs are presented as sequences of games, as used by cryptographers [22, 66, 67]: the initial game represents the protocol to prove; the goal is to bound the probability of breaking a certain security property in this game; intermediate games are obtained each from the previous one by transformations such that the difference of probability between consecutive games can easily be bounded; the final game is such that the desired probability is obviously bounded from the form of the game. (In general, it is simply 0 in that game.) The desired probability can then be easily bounded in the initial game. We represent games in a process calculus defining oracles interacting with an adversary. This calculus tries to mimick how classical cryptographic games are defined.

In this calculus, messages are bitstrings, and cryptographic primitives are functions from bitstrings to bitstrings. The calculus has a probabilistic semantics. The main tool for specifying security properties is indistinguishability: $Q$ is indistinguishable from $Q'$ up to probability $p$, $Q \approx_p Q'$, when the adversary has probability at most $p$ of distinguishing $Q$ from $Q'$. With respect to previous calculi used for representing cryptographic games, our calculus introduces an important novelty which is key for the automatic proof of security protocols: the values of all variables during the execution of a process are stored in arrays. For instance, $x[i]$ is the value of $x$ in the $i$-th copy of the process that defines $x$. Arrays represent global variables that are shared between all processes, and each cell can be given a value by a process for instance through an assignment or a random sampling. After being given a value, cells cannot be updated anymore. Arrays replace lists often used by cryptographers in their manual proofs of protocols. For example, consider the standard security assumption on a message authentication code (MAC). Informally, this definition says that the adversary has a negligible probability of forging a MAC, that is, that all correct MACs have been computed by calling the MAC oracle (i.e., function). So, in cryptographic proofs, one defines a list containing the arguments of calls to the MAC oracle, and when checking a MAC of a message $m$, one can additionally check that $m$ is in this list, with a negligible change in probability. In our calculus, the arguments of the MAC oracle are stored in arrays, and we perform a lookup in these arrays in order to find the message $m$. Arrays make it easier to automate proofs since they are always present in the calculus: one does not need to add explicit instructions to insert values in them, in contrast to the lists used in manual proofs. Therefore, many trivially sound but difficult to automate syntactic transformations disappear. Furthermore, relations between elements of arrays can easily be expressed by equalities, possibly involving computations on array indices.

CryptoVerif relies on a collection of game transformations, in order to transform the initial protocol into a game on which the desired security property is obvious. The most important kind of transformations exploits the security assumptions on cryptographic primitives in order to obtain a simpler game. As described in Section 5.2, these transformations can be specified in a generic way: we represent the security assumption of each cryptographic primitive by an
observational equivalence $L \approx_p R$, where the processes $L$ and $R$ encode oracles: they receive the arguments of the oracle and return its result. Then, the prover can automatically transform a process $Q$ that calls the oracles of $L$ (more precisely, contains as subterms terms that perform the same computations as oracles of $L$) into a process $Q'$ that calls the oracles of $R$ instead. We have used this technique to specify several variants of shared-key and public-key encryption, signature, message authentication codes, hash functions, Diffie-Hellman key agreement, simply by giving the appropriate equivalence $L \approx_p R$ to the prover. Other game transformations are syntactic transformations, used in order to be able to apply an assumption on a cryptographic primitive, or to simplify the game obtained after applying such an assumption.

In order to prove protocols, these game transformations are organized using a proof strategy based on advice: when a transformation fails, it suggests other transformations that should be applied before, in order to enable the desired transformation. Thanks to this strategy, simple protocols can often be proved in a fully automatic way. For delicate cases, CryptoVerif has an interactive mode, in which the user can manually specify the transformations to apply. It is often sufficient to specify a few well-chosen case distinctions and transformations coming from the security assumptions of primitives, by indicating the concerned cryptographic primitive and the concerned secret key if any; the prover infers the intermediate syntactic transformations by the advice strategy. This mode is helpful for instance for proving some public-key protocols, in which several security assumptions on primitives can be applied, but only one leads to a proof of the protocol. Importantly, CryptoVerif is always sound: whatever indications the user gives, when the prover shows a security property of the protocol, the property indeed holds assuming the given assumptions on the cryptographic primitives.

Finally, as we demonstrate in the rest of the this document, CryptoVerif is post-quantum sound: when the used cryptographic assumptions are valid for quantum adversaries, the proofs hold for quantum adversaries. The game transformations performed by CryptoVerif are valid not only against a classical probabilistic Turing-machine adversary, but also against a quantum adversary. More generally, they are valid against any kind of interactive black-box adversary that can simulate bounded time probabilistic Turing machines, limited by the cryptographic assumptions.

In addition to the oracle-based process calculus, CryptoVerif also allows to define games in a channel-based process calculus inspired by the applied pi calculus [1,2] and by the calculi of [59] and of [55]. The channel-based calculus is presented in Section 2.6 with a translation to the oracle-based calculus. The channel-based calculus was the initial version of the calculus used by CryptoVerif, as detailed in a previous report [29]. Future developments will use the oracle-based calculus with the semantics presented in this document. This language allowed us to prove the post-quantum soundness of CryptoVerif. It is closer to classical computational proofs and paves the way for important extensions, such as sharing parts of the code in calls to internal oracles, composition results, and loops implemented by recursive oracle calls, as it is easier to inline oracle calls than channel communications.

CryptoVerif has been implemented in OCaml (more than 60000 lines of code) and is available at http://cryptoverif.inria.fr/.

**Related Work** Various methods have been proposed for verifying security protocols in the computational model. Following the seminal paper by Abadi and Rogaway [3], many results show the soundness of the Dolev-Yao model with respect to the computational model, which makes it possible to use Dolev-Yao provers in order to prove protocols in the computational model (see, e.g., [7,37,41,42,50] and the survey [40]). However, these results have limitations, in particular in terms of allowed cryptographic primitives (they must satisfy strong security properties so that they correspond to Dolev-Yao style primitives), and they require some restrictions on
protocols (such as the absence of key cycles). A tool [39] was developed based on [41] to obtain computational proofs using the formal verifier AVISPA, for protocols that rely on public-key encryption and signatures.

Several frameworks exist for formalizing proofs of protocols in the computational model. Backes, Pfitzmann, and Waidner [9, 10] designed an abstract cryptographic library and showed its soundness with respect to computational primitives, under arbitrary active attacks. This framework has been used for a computationally-sound machine-checked proof of the Needham-Schroeder-Lowe protocol [70, 71]. Canetti [34] introduced the notion of universal composability. With Herzog [36], they show how a Dolev-Yao-style symbolic analysis can be used to prove security properties of protocols within the framework of universal composability, for a restricted class of protocols using public-key encryption as only cryptographic primitive. Then, they use the automatic Dolev-Yao verification tool ProVerif [24] for verifying protocols in this framework. Process calculi have been designed for representing cryptographic games, such as the probabilistic polynomial-time calculus of [59] and the cryptographic lambda-calculus of [62]. Logics have also been designed for proving security protocols in the computational model, such as the computational variant of PCL (Protocol Composition Logic) [46, 47] and CIL (Computational Indistinguishability Logic) [13]. Canetti et al. [35] use the framework of time-bounded task-PIOAs (Probabilistic Input/Output Automata) to prove security protocols in the computational model. This framework makes it possible to combine probabilistic and non-deterministic behaviors. These frameworks can be used to prove security properties of protocols in the computational sense, but except for [36] which relies on a Dolev-Yao prover, they have not been automated up to now, as far as we know.

Several techniques have been used for directly mechanizing proofs in the computational model. Type systems [45, 55, 57, 69] provide computational security guarantees. For instance, [55] handles shared-key and public-key encryption, with an unbounded number of sessions, by relying on the Backes-Pfitzmann-Waidner library. A type inference algorithm is given in [8]. The recent tool OWL [48] also relies on a type system that provides computational security guarantees. It supports MACs, public-key signatures, authenticated symmetric and public key encryption, random oracles, and the gap Diffie-Hellman assumption [63]. It can prove secrecy and integrity properties. In another line of research, a specialized Hoare logic was designed for proving asymmetric encryption schemes in the random oracle model [43, 44].

The tool CertiCrypt [14, 15, 17, 19, 20] enables the machine-checked construction and verification of cryptographic proofs by sequences of games [22, 68]. It relies on the general-purpose proof assistant Coq, which is widely believed to be correct. Nowak et al. [5, 60, 61] follow a similar idea by providing Coq proofs for several cryptographic primitives. More recently, frameworks for cryptographic proofs in Coq, FCF [64], and in Isabelle, CryptHOL [18], have been designed and used for proving cryptographic schemes. EasyCrypt [16], the successor of CertiCrypt, no longer generates Coq proofs, but provides a higher automation level by relying on SMT solvers, which makes the tool easier to use. Even if it focuses more on cryptographic primitives and schemes than on protocols, it has been used for proving some protocols such as one-round key exchange [12], e-voting [38], AWS key management [6], and distance bounding [31]. These frameworks and tools can perform more subtle reasoning than CryptoVerif, at the cost of more user effort: the user has to give all games and guide the proof that the games are indistinguishable. That becomes tedious for large protocols, which require many large games.

The tool Squirrel [11] relies on a computationally sound logic that allows to write interactive proofs of, e.g., stateful protocols. Still, it currently proves a security notion weaker than the standard one: the number of sessions of the protocol must be bounded independently of the security parameter (instead of being polynomial in the security parameter).

Independently, we have built the tool CryptoVerif [26] to help cryptographers, not only for
the verification, but also by generating the proofs by sequences of games [22,68], automatically
or with little user interaction. In particular, CryptoVerif generates the games, possibly using the
indications of which transformations to perform. This tool extends considerably early work by
Laud [53,54] which was limited either to passive adversaries or to a single session of the protocol.
More recently, Tšahhirov and Laud [56, 72] developed a tool similar to CryptoVerif but that
represents games by dependency graphs. It handles public-key and shared-key encryption and
proves secrecy properties; it does not provide bounds on the probability of success of an attack.

**Outline** The next section presents our process calculus for representing games, with its syntax, type system, formal semantics, as well as the definition of security properties. Section 3 collects information about games and reasons using it. Section 4 gives criteria for proving security properties of protocols. Section 5 describes the game transformations that we use for proving protocols. Section 6 explains how the prover chooses which transformation to apply at each point.

**Notations** We recall the following notations. We denote by {$M_1/x_1, \dots, M_m/x_m$} the substitution that replaces $x_j$ with $M_j$ for each $j \in \{1, \dots, m\}$. The cardinal of a set or multiset $S$ is denoted by $|S|$. Multisets $S$ are represented by functions that map each element $x$ of $S$ to the number of occurrences of $x$ in $S$, that is, when $S$ is a multiset, $S(x)$ is the number of elements of $S$ equal to $x$. We use $\cup$ for multiset union, defined by $(S_1 \cup S_2)(x) = S_1(x) + S_2(x)$. When $S$ and $S'$ are multisets, $\max(S, S')$ is the multiset such that $\max(S, S')(x) = \max(S(x), S'(x))$. The notation $\{x_1 \mapsto a_1, \dots, x_m \mapsto a_m\}$ designates the function that maps $x_j$ for $a_j$ for each $j \in \{1, \dots, m\}$ and is undefined for other inputs. When $f$ is a function, $f[x \mapsto a]$ is the function that maps $x$ to $a$ and all other elements as $f$. If $S$ is a finite set, $x \stackrel{R}{\leftarrow} S$ chooses a random element uniformly in $S$ and assigns it to $x$. If $\mathcal{A}$ is a probabilistic algorithm, $x \leftarrow \mathcal{A}(x_1, \dots, x_m)$ denotes the experiment of choosing random coins $r$ and assigning to $x$ the result of running $\mathcal{A}(x_1, \dots, x_m)$ with coins $r$. Otherwise, $x \leftarrow M$ is a simple assignment statement. If $D$ is a discrete probability distribution, we denote by $D(a)$ the probability that $X = a$, $\Pr[X = a]$, where $X$ is a random variable with probability distribution $D$, and we denote by $a \stackrel{R}{\leftarrow} D$ the random sampling of a value following the distribution $D$. We denote by $\text{Distr}(S)$ the set of discrete probability distributions over a set $S$. We denote by $\emptyset$ the empty stack, and a non empty stack $\mathcal{S}_t$ can be denoted by $a :: \mathcal{S}_t$, where $a$ is then the head of $\mathcal{S}_t$ and $\mathcal{S}_t$ its tail stack.

2 A Calculus for Cryptographic Games

2.1 Syntax and Informal Semantics

CryptoVerif represents games in the syntax of Figure 1. This syntax assumes a countable set of oracles names, denoted by $O$. It uses parameters, denoted by $n$, which are integers that bound the number of executions of oracles.

It also uses types, denoted by $T$, which are sets of values. So that types can be meaningfully
interpreted by an attacker, we assume that there exists an efficient bijection from the disjoint
union of all types to bitstrings. That implies in particular that all types are countable.

A type is *fixed* when it is the set of all bitstrings of a certain length; a type is *bounded* when it is a finite set. Particular types are predefined: *bool* = {*true*, *false*}, where *false* is 0 and *true* is 1; *bitstring* is the set of all bitstrings; *bitstring*⊥ = *bitstring* ∪ {*⊥*} where ⊥ is a special symbol; [*1*, *n*] is the set of integers {*1*, ..., *n*}, where *n* is a parameter. (We consider integers as bitstrings without leading zeroes.) We denote by *any* the specific type corresponding to the empty set of
<figure><img src="image_4.png" /><figcaption>Figure 1: Syntax for games</figcaption></figure>
values, which is thus contained in any other type. No other type can be empty, and *any* cannot be used within the syntax of the games.

The syntax also uses function symbols $f$. Each function symbol comes with a type declaration $f: T_1 \times \dots \times T_m \to T$, and represents an efficiently computable, deterministic function that maps each tuple in $T_1 \times \dots \times T_m$ to an element of $T$. Particular functions are predefined, and some of them use the infix notation: $M = N$ for the equality test, $M \neq N$ for the inequality test (both taking two values of the same type $T$ and returning a value of type *bool*), $M \lor N$ for the boolean or, $M \land N$ for the boolean and, $\neg M$ for the boolean negation (taking and returning values of type *bool*), tuples $(M_1, \dots, M_m)$ (taking values of any types and returning values of type *bitstring*); tuples are assumed to provide unambiguous concatenation, with tags for the types of $M_1, \dots, M_m$ so that tuples of different types are always different); test `if fun(M_1, M_2, M_3)` (with a first argument of type *bool* and the last two arguments of the same type $T$; it returns a value of type $T$: $M_2$ when $M_1$ is true and $M_3$ when $M_1$ is false).

In this syntax, terms represent computations on bitstrings. The replication index $i$ is an integer which serves in distinguishing different copies of a replicated oracle **foreach** $i \le n$ **do**. (Replication indices are typically used as array indices.) The variable access $x[M_1, \dots, M_m]$ returns the content of the cell of indices $M_1, \dots, M_m$ of the $m$-dimensional array variable $x$. We use $x, y, z, u$ as variable names. The function application $f(M_1, \dots, M_m)$ returns the result of applying function $f$ to $M_1, \dots, M_m$. Terms contain additional constructs which are very similar to those also included in oracle bodies and explained below. These constructs conclude by evaluating a term, instead of executing an oracle body. The construct **event_abort** $e$ executes event $e$ (without argument) and aborts the game.

The calculus distinguishes two kinds of processes, oracle definitions and oracle bodies.

An oracle definition $Q$ defines a set of parallel oracles ready to be called, each oracle being defined with a body $P$ that may end with a return value, followed by a potential new oracle definition $Q'$.

The oracle definition 0 defines no oracle; $Q \mid Q'$ is the parallel composition of $Q$ and $Q'$, it defines both oracles in $Q$ and in $Q'$; **foreach** $i \le n$ **do** $Q$ represents $n$ copies of $Q$ in parallel, each with a different value of $i \in [1, n]$; **newOracle** $O$; $Q$ creates a new private oracle $O$ and executes $Q$; this construct is useful in proofs, but does not occur in games manipulated by CryptoVerif. The oracle declaration $O[\tilde{i}](p) := P$ defines the oracles $O[\tilde{i}]$, where the indices $\tilde{i}$ are bound by the replications above the oracle declaration $O[\tilde{i}](p) := P$. The oracle $O[\tilde{i}]$ executes the oracle body $P$ when it is called with an argument that matches the pattern $p$. It will be explained in more detail below together with the semantics of the oracle call let $p = O[M_1, \dots, M_l, ?u_1[\tilde{i}] \le n_1, \dots, ?u_m[\tilde{i}] \le n_m](N)$ in $P$ else $P'$.

The oracle body construct $x[\tilde{i}] \stackrel{R}{\rightleftharpoons} T; P$ chooses a new random value in $T$, stores it in $x[\tilde{i}]$, and executes $P$. The abbreviation $\tilde{i}$ stands for a sequence of replication indices $i_1, \dots, i_m$. The random value is chosen according to the default distribution $D_T$ for type $T$, which is determined as follows:

* When the type $T$ is declared with option *nonuniform*, the default probability distribution $D_T$ for type $T$ may be non-uniform. It is left unspecified.

* Otherwise, if $T$ is *fixed*, $T$ consists of all bitstrings of a certain length, and the default distribution is the uniform distribution. The probability of each element of $T$ is $1/|T|$.

* If $T$ is *bounded* but not *fixed*, $T$ is finite, and the default distribution is an approximately uniform distribution, such that its distance to the uniform distribution is at most $\epsilon_T$. The
distance between two probability distributions $D_1$ and $D_2$ for type T is

$$d(D_1, D_2) = \frac{1}{2} \sum_{a \in T} |D_1(a) - D_2(a)|$$

Indeed, probabilistic Turing machines that run in bounded time cannot choose random elements exactly uniformly in sets whose cardinal is not a power of 2.

For example, a possible algorithm to obtain a random integer in $[0, m - 1]$ is to choose a random integer $x'$ uniformly among $[0, 2^k - 1]$ for a certain $k$ large enough and return $x'$ mod $m$. By euclidean division, we have $2^k = qm + r$ with $r \in [0, m - 1]$. With this algorithm

$$D(a) = \begin{cases} \frac{q+1}{2^k} & \text{if } a \in [0, r-1] \\ \frac{q}{2^k} & \text{if } a \in [r, m-1] \end{cases}$$

so

$$\left| D(a) - \frac{1}{m} \right| = \begin{cases} \frac{q+1}{2^k} - \frac{1}{m} & \text{if } a \in [0, r-1] \\ \frac{1}{m} - \frac{q}{2^k} & \text{if } a \in [r, m-1] \end{cases}$$

Therefore

$$d(D_T, uniform) = \frac{1}{2} \sum_{a \in T} \left| D(a) - \frac{1}{m} \right| = \frac{1}{2} r \left( \frac{q+1}{2^k} - \frac{1}{m} \right) - \frac{1}{2} (m-r) \left( \frac{1}{m} - \frac{q}{2^k} \right) \\ = \frac{r(m-r)}{m \cdot 2^k} \le \frac{m}{2^{k+1}}$$

so we can take $\epsilon_T = \frac{m}{2^{k+1}}$. A given precision of $\epsilon_T = \frac{1}{2^k}$ can be obtained by choosing $k = (k' + \text{number of bits of } m)$ random bits.

By default, CryptoVerif does not display $\epsilon_T$ in probability formulas, to make them more readable.

When $T$ is not declared with any of the options *nonuniform*, *fixed*, or *bounded*, CryptoVerif rejects the construct $x[i] \stackrel{R}{\leftarrow} T; P$. Function symbols represent deterministic functions, so all random numbers must be chosen by $x[i] \stackrel{R}{\leftarrow} T$. Deterministic functions make automatic syntactic manipulations easier: we can duplicate a term without changing its value.

The construct `let x[i] : T = M in P` stores the value of $M$ (which must be in $T$) in $x[i]$ and executes $P$. Furthermore, we say that a function $f : T_1 \times \dots \times T_m \to T$ is *efficiently injective* when it is injective and its inverses are efficiently computable, that is, there exist functions $f_j^{-1} : T \to T_j$ ($1 \le j \le m$) such that $f_j^{-1}(f(x_1, \dots, x_m)) = x_j$ and $f_j^{-1}$ is efficiently computable. When $f$ is efficiently injective, we define a pattern matching construct `let f(x_1, \dots, x_m) = M` in $P$ `else P'` as an abbreviation for `let y : T = M in let x'_1 : T_1 = f_1^{-1}(y) in \dots let x'_m : T_m = f_m^{-1}(y) in if f(x'_1, \dots, x'_m) = y then (let x'_1 : T_1 = x'_1 in \dots let x'_m : T_m = x'_m in P) else P'` where $y, x'_1, \dots, x'_m$ are fresh variables. (The variables $x'_1, \dots, x'_m$ are introduced to make sure that none of the variables $x_1, \dots, x_m$ is defined when the pattern-matching fails.) We naturally generalize this construct to `let p = M in P` `else P'` where $p$ is built from variables, efficiently injective functions, and equality tests. When $p$ is simply a variable, the pattern-matching always succeeds, so the `else` branch of the assignment is never executed and can be omitted. In this case, the alternative syntax $x \leftarrow M; P$ is a synonym for `let x = M in P`.

The construct `event e(M_1, \dots, M_l); P` executes the event $e(M_1, \dots, M_l)$, then runs $P$. This event records that a certain program point has been reached with certain values of $M_1, \dots, M_l$,
but otherwise does not affect the execution of the oracle. Events are used in particular for specifying security properties.

The construct **event_abort** *e* executes event *e* (without argument) and aborts the game.

Next, we explain the construct find[unique?] ($\bigoplus_{j=1}^m u_{j1}[\tilde{i}] = i_{j1} \le n_{j1}, \dots, u_{jm_j}[\tilde{i}] = i_{jm_j} \le n_{jm_j}$ **suchthat** defined($M_{j1}, \dots, M_{j_l}$) $\land$ $M_j$ **then** $P_j$) **else** $P$. The order and array indices on tuples are taken component-wise, so for instance, $u_{j1}[\tilde{i}] = i_{j1} \le n_{j1}, \dots, u_{jm_j}[\tilde{i}] = i_{jm_j} \le n_{jm_j}$ can be further abbreviated $\tilde{u}_j[\tilde{i}] = \tilde{i}_j \le \tilde{n}_j$. A simple example is the following: find $u = i \le n$ **suchthat** defined($x[i]$) $\land$ $x[i] = a$ **then** $P'$ **else** $P$ tries to find an index $i$ such that $x[i]$ is defined and $x[i] = a$, and when such an $i$ is found, it stores it in $u$ and executes $P'$ with that value of $u$; otherwise, it executes $P$. In other words, this find construct looks for the value $a$ in the array $x$, and when $a$ is found, it stores in $u$ an index such that $x[u] = a$. Therefore, the find construct allows us to access arrays, which is key for our purpose. More generally, find $u_1[\tilde{i}] = i_1 \le n_1, \dots, u_m[\tilde{i}] = i_m \le n_m$ **suchthat** defined($M_1, \dots, M_l$) $\land$ $M$ **then** $P'$ **else** $P$ tries to find values of $i_1, \dots, i_m$ for which $M_1, \dots, M_l$ are defined and $M$ is true. In case of success, it stores the obtained values in $u_1[\tilde{i}], \dots, u_m[\tilde{i}]$ and executes $P'$. In case of failure, it executes $P$. This is further generalized to $m$ branches: find ($\bigoplus_{j=1}^m u_{j1}[\tilde{i}] = i_{j1} \le n_{j1}, \dots, u_{jm_j}[\tilde{i}] = i_{jm_j} \le n_{jm_j}$ **suchthat** defined($M_{j1}, \dots, M_{j_l}$) $\land$ $M_j$ **then** $P_j$) **else** $P$ tries to find a branch $j$ in $[1, m]$ such that there are values of $i_{j1}, \dots, i_{jm_j}$ for which $M_{j1}, \dots, M_{j_l}$ are defined and $M_j$ is true. In case of success, it stores them in $u_{j1}[\tilde{i}], \dots, u_{jm_j}[\tilde{i}]$ and executes $P_j$. In case of failure for all branches, it executes $P$. More formally, it evaluates the conditions defined($M_{j1}, \dots, M_{j_l}$) $\land$ $M_j$ for each $j$ and each value of $i_{j1}, \dots, i_{jm_j}$ in $[1, n_{j1}] \times \dots \times [1, n_{jm_j}]$. If none of these conditions is true, it executes $P$. Otherwise, it chooses randomly one $j$ and one value of $i_{j1}, \dots, i_{jm_j}$ such that the corresponding condition is true, according to the distribution $D_{find}(S)$ where $S$ is the set of possible solutions $j, i_{j1}, \dots, i_{jm_j}$, stores it in $u_{j1}[\tilde{i}], \dots, u_{jm_j}[\tilde{i}]$, and executes $P_j$. The distribution $D_{find}(S)$ is almost uniform: formally, the distance between $D_{find}(S)$ and the uniform distribution is at most $\epsilon_{find}/2$, that is, $d(D_{find}(S), uniform) \le \epsilon_{find}/2$, that is, $\frac{1}{2} \sum_{v \in S} |D_{find}(S)(v) - \frac{1}{|S|}| \le \epsilon_{find}/2$, so that, when $|S| = |S'|$, for any bijection $\phi: S \to S'$, $\frac{1}{2} \sum_{v \in S} |D_{find}(S)(v) - D_{find}(S')(\phi(v))| \le \epsilon_{find}$. Moreover $D_{find}(S)(v_i) = D_{|S|}(i)$ where $S = \{v_1, \dots, v_{|S|}\}$ with the values $v_i$ ordered in increasing order lexicographically, for some distribution $D_{|S|}$ that depends only on the cardinal of $S$. In other words, the probability of a value $v_i$ in the distribution $D_{find}(S)$ does not depend on the values in the set $S$ but only on the number $|S|$ of elements of $S$ and on the position $i$ of the value $v_i$ in $S$ ordered in increasing order lexicographically. Therefore, transformations that do not modify the number of successful values nor their order, that is, transformations that map elements $v$ of $S$ to elements $\phi(v)$ of $S'$ at the same position $i$, preserve the probabilities exactly and we do not need to add $\epsilon_{find}$ to the probability when we apply such a transformation. This is true for instance when we remove a branch of find that is never taken. By default, CryptoVerif does not display $\epsilon_{find}$ in probability formulas, to make them more readable. We cannot take the first element found because the game transformations made by CryptoVerif may reorder the elements. For these transformations to preserve the behavior of the game, the distribution of the chosen element must be invariant by reordering, up to a small probability $\epsilon_{find}$. In this definition, the variables $i_{j1}, \dots, i_{jm_j}$ are considered as replication indices, while $u_{j1}[\tilde{i}], \dots, u_{jm_j}[\tilde{i}]$ are considered as array variables. The indication [unique?] stands for either [unique<sub>e</sub>] or empty. The empty case has just been explained. When the find is marked [unique<sub>e</sub>] and there are several solutions that make the condition of the find evaluate to true, we execute the event *e* and abort the game. When there is zero or one solution, the find is executed as when [unique?] is empty. This semantics allows us to perform game transformations that require the find to have a single solution.

The conditional if $M$ then $P$ else $P'$ executes $P$ if $M$ evaluates to true. Otherwise, it executes
$P'$. CryptoVerif also supports the conditional if $\mathit{defined}(M_1, \dots, M_l) \land M$ then $P$ else $P'$, which executes $P$ if $M_1, \dots, M_l$ are defined and $M$ evaluates to true. Otherwise, it executes $P'$. This conditional is internally encoded as find such that $\mathit{defined}(M_1, \dots, M_l) \land M$ then $P$ else $P'$. The conjunct $M$ can be omitted when it is true, writing if $\mathit{defined}(M_1, \dots, M_l)$ then $P$ else $P'$.

The constructs insert and get handle tables, used for instance to store the keys of the protocol participants. A table can be represented as a list of tuples; insert $\mathit{Tbl}(M_1, \dots, M_l); P$ inserts the element $M_1, \dots, M_l$ in the table $\mathit{Tbl}$; get $\mathit{Tbl}(x_1 : T_1, \dots, x_l : T_l)$ such that $M$ in $P$ else $P'$ tries to retrieve an element $(x_1, \dots, x_l)$ in the table $\mathit{Tbl}$ such that $M$ is true. When such an element is found, it executes $P$ with $x_1, \dots, x_l$ bound to that element. (When several such elements are found, one of them is chosen randomly according to distribution $D_{\mathit{get}}(S)$ where $S$ is the set of indices of suitable elements, with $d(D_{\mathit{get}}(S), \mathit{uniform}) \le \epsilon_{\mathit{find}}/2$.) When no such element is found, $P'$ is executed. We can generalize this construct to patterns instead of variables similarly to the let case. As in the case of find, the indication $[\mathit{unique}]$ stands for either $[\mathit{unique}_e]$ or empty. The empty case has just been explained. When the get is marked $[\mathit{unique}_e]$ and there are several solutions, we execute the event $e$ and abort the game. When there is zero or one solution, the get is executed as when $[\mathit{unique}]$ is empty. CryptoVerif internally translates the insert and get constructs into find.

Let us explain the return ($N$), yield, and oracle call commands. A semantic configuration always contains an oracle execution stack, the head oracle being the one currently executed and the stack corresponding to the nested calls. It also contains a set of callable oracles.

Whenever we encounter an oracle declaration $O[\tilde{i}](p) := P$, this oracle is added to the set of callable oracles. Intuitively, it is then possible to call this oracle for the given indices and with an argument that matches the pattern $p$. In the following, we will consider that all oracle declarations are of the form $O[\tilde{i}](x[\tilde{i}] : T) := P$, where we encode the input pattern for $O[\tilde{i}](p) := P$ as $O[\tilde{i}](x[\tilde{i}] : T) := \mathit{let } p = x \mathit{ in } P \mathit{ else } yield$.

Whenever the head oracle executes an oracle call let $x[\tilde{i}] : T = O[M_1, \dots, M_l](N)$ in $P$ else $P'$, one looks for an available oracle $O[a_1, \dots, a_l]$ where $M_1, \dots, M_l$ evaluate to $a_1, \dots, a_l$. (Terms $M_1, \dots, M_l$ are intuitively analogous to IP addresses and ports, which are numbers that the adversary may guess.) If no such callable oracle is found, the execution blocks. Otherwise, by the invariants given below, there is at most one such oracle $O[a_1, \dots, a_l](x'[\tilde{i}'] : T') := P''$. This oracle is then executed: the argument $N$ is evaluated and stored in $x'[\tilde{i}']$ if it is in $T'$ (otherwise the execution blocks). The well-typed condition is not a restriction for the attacker, as it can always use type conversion functions.

Finally, the oracle $O[a_1, \dots, a_l](x'[\tilde{i}'] : T') := P''$ is removed from the set of callable oracles, the body $P''$ of the called oracle is pushed on top of the stack, and executed. In this situation, we then have a new oracle body currently being executed, and the second one in the stack is the latest oracle call let $x[\tilde{i}] : T = O[M_1, \dots, M_l](N)$ in $P$ else $P'$ waiting for a return value.

When an oracle performs a return command return ($N'$); $Q$, it returns normally, and the in branch of the caller is executed. In more details, we pop the return command from the execution stack. The head of the execution stack is then the latest oracle call, of the form let $x[\tilde{i}] : T = O[M_1, \dots, M_l](N)$ in $P$ else $P'$. We evaluate $N'$, store it in $x[\tilde{i}]$ if it is in $T$ and continue the execution with $P$, in a similar fashion to an assignment. The oracles in $Q$, which follow the executed return command, are added to the set of callable oracles.

When an oracle performs a yield command, it returns abnormally, and the else branch of the caller is executed. In more detail, we also pop the yield command from the execution stack. The head of the execution stack is then the latest oracle call, of the form let $x[\tilde{i}] : T = O[M_1, \dots, M_l](N)$ in $P$ else $P'$, and we execute $P'$.

In the case of an oracle call with pattern matching let $p = O[M_1, \dots, M_l](N)$ in $P$ else $P'$, the pattern-matching is encoded as in assignments. The oracle body $P'$ is executed in case the
pattern-matching fails. We note that in contrast to the assignment encoding, we still need an else branch for the specific failure case of *yield* that cannot be encoded with a conditional. Oracles that take several arguments or return several results are encoded using tuples and pattern-matching on tuples.

Oracle calls can be made with some unspecified indices, following the syntax

$$ \text{let } x[\tilde{i}] : T = O[M_1, \dots, M_l, ?u_1[\tilde{i}] \le n_1, \dots, ?u_m[\tilde{i}] \le n_m](N) \text{ in } P \text{ else } P'. $$

In this case, we evaluate $M_1, \dots, M_l$ to $a_1, \dots, a_l$, and consider the set $S$ of oracles $O[a_1, \dots, a_l, b_1, \dots, b_m]$ among the set of callable oracles. We choose one of these oracles randomly following the probability distribution $D_{\text{call}}(S)$, which is approximately uniform like $D_{\text{find}}(S)$. Then we perform the call as explained above. In the remainder of the execution, $?u_1[\tilde{i}], \dots, ?u_m[\tilde{i}]$ are bound to $b_1, \dots, b_m$. In a call to oracle $O$, only indices corresponding to replications that are directly above the oracle declaration of $O$ can be unspecified. Indices that are used inside a previous oracle definition must then be explicitly specified. For instance, if oracle $O_2$ is defined by

$$ \text{foreach } i_1 \le n_1 \text{ do } O_1[i_1](p_1) := \dots \text{ return } (N); \text{foreach } i_2 \le n_2 \text{ do } O_2[i_1, i_2](p_2) := \dots $$

in call to $O_2$, the first index $i_1$ must always be explicitly specified by a term $M_1$; the second index may either be specified by a term $M_2$ or left unspecified by $?u_2[\tilde{i}] \le n_2$.

The execution depends on a parametric attacker $\mathcal{A}$. Whenever the execution stack is empty, the attacker can perform an oracle call, and the attacker receives the return of the last oracle in the stack. Oracle $O$ can be declared private with newOracle $O$, in which case only oracles under the scope of newOracle $O$ can call $O$, and in particular the attacker cannot. (This is useful in the proofs, although all oracles of protocols are often public.) In effect, the attacker can then be seen as controlling the network between communicating oracles.

An else branch of find, if, get, or let may be omitted when it is else yield. (Note that “else 0” would not be syntactically correct.) Similarly, ?yield may be omitted after event, $\leftarrow^R$, or insert and in yield may be omitted after let. A trailing 0 after a return may be omitted. We also omit oracle parameters and replication indices if there are none.

The current replication indices at a certain program point in a process are the replication indices $i_1, \dots, i_m$ bound by replications and find above that program point. The replication `foreach i \le n \ do Q` binds the replication index $i$ in $Q$. The find construct

$$ \begin{array}{l} \text{find}[\text{unique?}] (\bigoplus_{j=1}^m u_{j1}[\tilde{i}] = i_{j1} \le n_{j1}, \dots, u_{jm_j}[\tilde{i}] = i_{jm_j} \le n_{jm_j} \text{ such that} \\ \quad \text{defined}(M_{j1}, \dots, M_{jl_j}) \land M_j \text{ then } \dots) \\ \text{else } \dots \end{array} $$

binds the replication indices $i_{j1}, \dots, i_{jm_j}$ in $\text{defined}(M_{j1}, \dots, M_{jl_j}) \land M_j$. We often abbreviate $x[i_1, \dots, i_m]$ by $x$ when $i_1, \dots, i_m$ are the current replication indices at the definition of $x$, but it should be kept in mind that this is only an abbreviation. Variables defined under a replication must be arrays: for example `foreach i_1 \le n_1 \ do \dots \foreach i_m \le n_m \ do \text{let } x[i_1, \dots, i_m] : T = M \ in \dots` More formally, we require the following invariant:

**Invariant 1 (Single definition)** The oracle definition $Q_0$ satisfies Invariant 1 if and only if

1. in every definition of $x[i_1, \dots, i_m]$ in $Q_0$, the indices $i_1, \dots, i_m$ of $x$ are the current replication indices at that definition, and
2. two different definitions of the same variable $x$ in $Q_0$ are in different branches of a find, if (or let), oracle call, or get.

In a let with pattern-matching, let $p = M$ in P else P', the variables bound by $p$ are considered to be defined in the in branch; however, the variables defined in $M$ and in terms included in the pattern $p$ are defined before the branching.

Similarly, in an oracle call, let $p = O[M_1, \dots, M_l, ?u_1[\tilde{i}] \le n_1, \dots, ?u_m[\tilde{i}] \le n_m](N)$ in P else P', the variables bound by $p$ are considered to be defined in the in branch; however, the variables defined in $N$, $M_1, \dots, M_l$ and in terms included in the pattern $p$ as well as the variables $u_1, \dots, u_m$ are defined before the branching.

In get[unique?] Tbl($p_1, \dots, p_l$) suchthat $M$ in P else P', the variables bound by $p_j$ for $j \le l$ and the variables defined in $M$ and in terms included in the patterns $p_j$ are (temporarily) defined before the branching.

Invariant 1 guarantees that each variable is assigned at most once for each value of its indices. (Indeed, item 2 shows that only one definition of each variable can be executed for given indices in each trace.) A definition of $x[\tilde{i}]$ can be $x[\tilde{i}] \stackrel{R}{\leftarrow} T$, a let, get, or oracle declaration that contains the pattern $x[\tilde{i}] : T$, the construct find... $x[\tilde{i}] = i \le n...$, or the oracle call let $p = O[M_1, \dots, M_l, ?u_1[\tilde{i}] \le n_1, \dots, ?u_m[\tilde{i}] \le n_m](N)$ in P else P' where $p$ contains the pattern $x[\tilde{i}] : T$ or when $x[\tilde{i}]$ is $u_j[\tilde{i}]$ for some $j \le m$.

**Invariant 2 (Defined variables)** The oracle definition $Q_0$ satisfies Invariant 2 if and only if every occurrence of a variable access $x[M_1, \dots, M_m]$ in $Q_0$ is either

* syntactically under the definition of $x[M_1, \dots, M_m]$ (in which case $M_1, \dots, M_m$ are in fact the current replication indices at the definition of $x$);

* or in a defined condition in a find command or term;

* or in $M'_j$ in a process or term of the form find ($\bigoplus_{j=1}^{m''} \tilde{u}_j[\tilde{i}] = \tilde{i}_j \le \tilde{n}_j$ suchthat defined($M'_{j1}, \dots, M'_{j l_j}$) $\land$ $M'_j$ then $P_j$) else P where for some $k \le l_j$, $x[M_1, \dots, M_m]$ is a subterm of $M'_{jk}$.

* or in $P_j$ in a process or term of the form find ($\bigoplus_{j=1}^{m''} \tilde{u}_j[\tilde{i}] = \tilde{i}_j \le \tilde{n}_j$ suchthat defined($M'_{j1}, \dots, M'_{j l_j}$) $\land$ $M'_j$ then $P_j$) else P where for some $k \le l_j$, there is a subterm $N$ of $M'_{jk}$ such that $N\{\tilde{u}_j[\tilde{i}]/\tilde{i}_j\} = x[M_1, \dots, M_m]$.

Invariant 2 guarantees that variables can be accessed only when they have been initialized. It checks that the definition of the variable access is either in scope (first item) or checked by a find (last two items). The scope of variable definitions is defined as follows: $x[\tilde{i}]$ is syntactically under its definition when it is

* inside $P$ in $x[\tilde{i}] \stackrel{R}{\leftarrow} T; P$;

* inside $N$ in $x[\tilde{i}] \stackrel{R}{\leftarrow} T; N$;

* inside $P$ in let $p = M$ in P else P' when $x[\tilde{i}] : T$ is bound in the pattern $p$;

* inside $N$ in let $p = M$ in $N$ else $N'$ when $x[\tilde{i}] : T$ is bound in the pattern $p$;

* inside $N$ in let $x[\tilde{i}] : T = M$ in $N$;
* inside $P_j$ in find[unique?] ($\bigoplus_{j=1}^m u_{j1}[\tilde{i}] = i_{j1} \le n_{j1}, \dots, u_{jm_j}[\tilde{i}] = i_{jm_j} \le n_{jm_j}$ such that defined($M_{j1}, \dots, M_{jlt_j}$) $\land$ $M_j$ then $P_j$) else $P$ when $x$ is $u_{jk}$ for some $k \le m_j$;

* inside $N_j$ in find[unique?] ($\bigoplus_{j=1}^m u_{j1}[\tilde{i}] = i_{j1} \le n_{j1}, \dots, u_{jm_j}[\tilde{i}] = i_{jm_j} \le n_{jm_j}$ such that defined($M_{j1}, \dots, M_{jlt_j}$) $\land$ $M_j$ then $N_j$) else $N$ when $x$ is $u_{jk}$ for some $k \le m_j$;

* inside $M$ or $P$ in get[unique?] $Tbl(p_1, \dots, p_l)$ such that $M$ in $P$ else $P'$ when $x[\tilde{i}] : T$ is bound in one of the patterns $p_1, \dots, p_l$;

* inside $M$ or $N$ in get[unique?] $Tbl(p_1, \dots, p_l)$ such that $M$ in $N$ else $N'$ when $x[\tilde{i}] : T$ is bound in one of the patterns $p_1, \dots, p_l$;

* inside $P$ in $O[\tilde{i}](p) := P$ when $x[\tilde{i}] : T$ is bound in the pattern $p$.

* inside $P$ in let $p = O[M_1, \dots, M_l, ?u_1[\tilde{i}] \le n_1, \dots, ?u_m[\tilde{i}] \le n_m](N)$ in $P$ else $P'$ when $x[\tilde{i}] : T$ is bound in the pattern $p$, or when $x$ is $u_m$ for some $j \le m$.

A variable access that does not correspond to the first item of Invariant 2 is called an *array access*. We furthermore require the following invariant. In this invariant, we consider a finite set of public variables $V$: these variables are defined in the considered oracle definition $Q_0$ (though it may sometimes happen that they are never defined) and can be accessed by the adversary via the find construct.

**Invariant 3 (Variables defined in find and get conditions)** The oracle definition $Q_0$ satisfies Invariant 3 with public variables $V$ if and only if the variables defined in conditions of find and the variables defined in patterns and in conditions of get have no array accesses and are not in the set of variables $V$.

These conditions are needed for variables of get, because they will be transformed into variables defined in conditions of find by the transformation of get into find.

**Invariant 4 (Terms in find and get conditions)** The oracle definition $Q_0$ satisfies Invariant 4 if and only if event and insert do not occur in conditions of find and get.

Invariant 4 guarantees that evaluating the condition of a find or get does not change the state of the system.

**Definition 1** A term is *simple* when it contains only replication indices, variables, and function applications.

**Invariant 5 (Terms in defined conditions)** The oracle definition $Q_0$ satisfies Invariant 5 if and only if the terms $M_1, \dots, M_l$ in conditions defined($M_1, \dots, M_l$) in find are simple.

Terms that are not simple are handled by expanding them into their corresponding oracle body commands. Invariant 5 is needed because terms in defined conditions cannot be expanded (see the transformation *expand* in Section 5.1.3). By combining this invariant with Invariant 2, we see that the terms of all variable accesses $x[M_1, \dots, M_m]$ are simple.

**Invariant 6 (Events)** We distinguish three disjoint sets of events $e$, Shoup events, non-unique events, and other events. The oracle definition $Q_0$ satisfies Invariant 6 if and only if

* Shoup events occur only in processes or terms of the form `event_abort e` in $Q_0$,
* non-unique events occur only in find[unique<sub>e</sub>] or get[unique<sub>e</sub>] in Q<sub>0</sub>, and

* other events occur in event e(M<sub>1</sub>, ..., M<sub>t</sub>) or in event_abort e in Q<sub>0</sub>.

The name “Shoup events” is used because these events are introduced when applying Shoup’s lemma [68] (see Section 5.1.12). The non-unique events are those triggered when a find[unique<sub>e</sub>] or get[unique<sub>e</sub>] actually has several solutions.

To provide an invariant expressing that oracles for a given name are defined only once, we define the following multiset by induction on oracle definitions and bodies:

$$Defined^O(0) = \emptyset$$

$$Defined^O(Q_1 | Q_2) = Defined^O(Q_1) \cup Defined^O(Q_2)$$

$$Defined^O(\text{foreach } i \le n \text{ do } Q) = Defined^O(Q)$$

$$Defined^O(O[\tilde{i}](x[\tilde{i}] : T) := P) = \{O\} \cup Defined^O(P)$$

$$Defined^O(\text{newOracle } O; Q) = Defined^O(Q) \setminus \{O\}$$

$$Defined^O(C[Q_1, \dots, Q_k]) = \max_{j=1}^{k} Defined^O(Q_j)$$

Here, we denote by C an oracle body context, that is, a context with only oracle body constructs and several holes for oracle definitions as possible continuations, and C[Q<sub>1</sub>, ..., Q<sub>k</sub>] corresponds to instantiating the continuations with the given processes. We use C[Q<sub>1</sub>, ..., Q<sub>k</sub>] to define by induction the function at once for all oracle body constructs.

**Invariant 7 (Single Oracle definition)** The oracle definitions Q<sub>0</sub> satisfies Invariant 7 if and only if

1. in every oracle declaration of O[\tilde{i}](p) in Q<sub>0</sub>, the indices \tilde{i} of O are the current replication indices at that declaration, and

2. Defined<sup>O</sup>(Q<sub>0</sub>) does not contain duplicate elements.

Similar to the invariant 1 for variables, we guarantee that each oracle is correctly defined at most once. Thanks to this invariant, we can omit the indices of oracles in oracle declarations, writing O(p) := P for O[\tilde{i}](p) := P where \tilde{i} are the current replication indices at that declaration.

All these invariants are checked by the prover for the initial game and preserved by all game transformations.

We denote by var(P) the set of variables that occur in P, vardef(P) the set of variables defined in P (var(P) may contain more variables than vardef(P) in case some variables are read using find but never defined), and by fo(P) the set of free oracles of P. (We use similar notations for oracle definitions.)

## 2.2 Example

Let us introduce two cryptographic primitives that we use below.

**Definition 2** Let T<sub>mk</sub> and T<sub>ms</sub> be types that correspond intuitively to keys and message authentication codes, respectively; T<sub>mk</sub> is a fixed-length type. A message authentication code scheme MAC [21] consists of two function symbols:
* mac : bitstring × $T_{mk} \to T_{ms}$ is the MAC algorithm taking as arguments a message and a key, and returning the corresponding tag. (We assume here that mac is deterministic; we could easily encode a randomized mac by adding random coins as an additional argument.)

* verify : bitstring × $T_{mk} \times T_{ms} \to \mathit{bool}$ is a verification algorithm such that $\mathit{verify}(m, k, t) = \text{true}$ if and only if $t$ is a valid MAC of message $m$ under key $k$. (Since mac is deterministic, $\mathit{verify}(m, k, t)$ is typically $\mathit{mac}(m, k) = t$.)

We have $\forall m \in \mathit{bitstring}, \forall k \in T_{mk}, \mathit{verify}(m, k, \mathit{mac}(m, k)) = \text{true}$.

The advantage of an adversary against unforgeability under chosen message attacks (UF-CMA) is

$$ \mathbf{Succ}_{\mathbf{MAC}}^{\mathbf{uf-cma}}(t, q_m, q_v, l) = \max_{\mathcal{A}} \Pr \left[ \begin{array}{l} k \stackrel{R}{\leftarrow} T_{mk}; (m, s) \leftarrow \mathcal{A}^{\mathit{mac}(.,k),\mathit{verify}(.,k,.)} : \mathit{verify}(m, k, s) \\ \wedge \text{m was never queried to the oracle } \mathit{mac}(., k) \end{array} \right] $$

where the adversary $\mathcal{A}$ is any probabilistic Turing machine that runs in time at most $t$, calls $\mathit{mac}(., k)$ at most $q_m$ times with messages of length at most $l$, and calls $\mathit{verify}(., k, .)$ at most $q_v$ times with messages of length at most $l$.

$\mathbf{Succ}_{\mathbf{MAC}}^{\mathbf{uf-cma}}(t, q_m, q_v, l)$ is the probability that an adversary forges a MAC, that is, returns a pair $(m, s)$ where $s$ is a correct MAC for $m$, without having queried the MAC oracle $\mathit{mac}(., k)$ on $m$. Intuitively, when the MAC is secure, this probability is small: the adversary has little chance of forging a MAC. Hence, the MAC guarantees the integrity of the MACed message because one cannot compute the MAC without the secret key.

Two frameworks exist for expressing security properties. In the asymptotic framework, used in [25, 26], the length of keys is determined by a security parameter $\eta$, and a MAC is UF-CMA when $\mathbf{Succ}_{\mathbf{MAC}}^{\mathbf{uf-cma}}(t, q_m, q_v, l)$ is a negligible function of $\eta$ when $t$ is polynomial in $\eta$. ($f(\eta)$ is negligible when for all polynomials $q$, there exists $\eta_o \in \mathbb{N}$ such that for all $\eta > \eta_o$, $f(\eta) \le \frac{1}{q(\eta)}$.) The assumption that functions are efficiently computable means that they are computable in time polynomial in $\eta$ and in the length of their arguments. The goal is to show that the probability of success of an attack against the protocol is negligible, assuming the parameters $n$ are polynomial in $\eta$ and the network messages are of length polynomial in $\eta$. In contrast, in the exact security framework, on which we focus in this report, one computes the probability of success of an attack against the protocol as a function of the probability of breaking the primitives such as $\mathbf{Succ}_{\mathbf{MAC}}^{\mathbf{uf-cma}}(t, q_m, q_v, l)$, of the runtime of functions, of the parameters $n$, and of the length of messages, thus providing a more precise security result. Intuitively, the probability $\mathbf{Succ}_{\mathbf{MAC}}^{\mathbf{uf-cma}}(t, q_m, q_v, l)$ is assumed to be small (otherwise, the computed probability of attack will be large), but no formal assumption on this probability is needed to establish the security theorem.

**Definition 3** Let $T_k, T_r$, and $T_e$ be types for random coins, keys, and ciphertexts respectively. $T_k$ and $T_r$ are fixed-length types. A symmetric encryption scheme SE [21] consists of two function symbols:

* enc : bitstring × $T_k \times T_r \to T_e$ is the encryption algorithm taking as arguments the cleartext, the key, and random coins, and returning the ciphertext,

* dec : $T_e \times T_k \to \mathit{bitstring}_{\perp}$ is the decryption algorithm taking as arguments the ciphertext and the key, and returning either the cleartext when decryption succeeds or $\perp$ when decryption fails,
such that $\forall k \in T_k, \forall m \in \text{bitstring}, \forall r \in T_r, \text{dec}(\text{enc}(m, k, r), k) = m$.

Let $LR(x, y, b) = x$ if $b = 0$ and $LR(x, y, b) = y$ if $b = 1$, defined only when $x$ and $y$ are bitstrings of the same length. The advantage of an adversary against indistinguishability under chosen plaintext attacks (IND-CPA) is

$$ \text{Succ}_{\text{SE}}^{\text{ind-cpa}}(t, q_e, l) = \max_{\mathcal{A}} 2 \Pr \left[ \begin{array}{l} b \stackrel{R}{\leftarrow} \{0, 1\}; k \stackrel{R}{\leftarrow} T_k; \\ b' \stackrel{R}{\leftarrow} \mathcal{A}^{\stackrel{R}{\leftarrow} T_r; \text{enc}(LR(\dots,b), k, r)} : b' = b \end{array} \right] - 1 $$

where $\mathcal{A}$ is any probabilistic Turing machine that runs in time at most $t$ and calls $r \stackrel{R}{\leftarrow} T_r; \text{enc}(LR(\dots,b), k, r)$ at most $q_e$ times on messages of length at most $l$.

Given two bitstrings $a_0$ and $a_1$ of the same length, the left-right encryption oracle $r \stackrel{R}{\leftarrow} T_r; \text{enc}(LR(\dots,b), k, r)$ returns $r \stackrel{R}{\leftarrow} T_r; \text{enc}(LR(a_0, a_1, b), k, r)$, that is, encrypts $a_0$ when $b = 0$ and $a_1$ when $b = 1$. $\text{Succ}_{\text{SE}}^{\text{ind-cpa}}(t, q_e, l)$ is the probability that the adversary distinguishes the encryption of the messages $a_0$ given as first arguments to the left-right encryption oracle from the encryption of the messages $a_1$ given as second arguments. Intuitively, when the encryption scheme is IND-CPA secure, this probability is small: the ciphertext gives almost no information on what the cleartext is (one cannot determine whether it is $a_0$ or $a_1$ without having the secret key).

**Example 1** Let us consider the following trivial protocol:

$$ A \to B : e, \text{mac}(e, x_{mk}) \quad \text{where } e = \text{enc}(x'_{k}, x_{k}, x_{r}) \\ \text{and } x_{r}, x'_{k} \text{ are fresh random numbers} $$

$A$ and $B$ are assumed to share a key $x_k$ for a symmetric encryption scheme and a key $x_{mk}$ for a message authentication code. $A$ creates a fresh key $x'_k$ and sends it encrypted under $x_k$ to $B$. A MAC is appended to the message, in order to guarantee integrity. In other words, the protocol sends the key $x'_k$ encrypted using an encrypt-then-MAC scheme [21]. The goal of the protocol is that $x'_k$ should be a secret key shared between $A$ and $B$. This protocol can be modeled in our calculus by the following oracle definition $Q_0$:

$$ \begin{align*} Q_0 = O_0() &:= x_k \stackrel{R}{\leftarrow} T_k; x_{mk} \stackrel{R}{\leftarrow} T_{mk}; \text{return } (); (Q_A | Q_B) \\ Q_A = \text{foreach } i \le n \text{ do } O_A() &:= x'_k \stackrel{R}{\leftarrow} T_k; x_r \stackrel{R}{\leftarrow} T_r; \\ & \text{let } x_m : \text{bitstring} = \text{enc}(\text{k2b}(x'_k), x_k, x_r) \text{ in return } (x_m, \text{mac}(x_m, x_{mk})) \\ Q_B = \text{foreach } i' \le n' \text{ do } O_B(x'_{m}, x_{ma}) &:= \text{if verify}(x'_{m}, x_{mk}, x_{ma}) \text{ then} \\ & \text{let } i_{\perp}(\text{k2b}(x''_{k})) = \text{dec}(x'_{m}, x_{k}) \text{ in return } () \end{align*} $$

When the oracle $O_0$ is called, it begins execution: it generates the keys $x_k$ and $x_{mk}$ randomly. Then it returns control to the adversary, and provides $n$ copies of oracles $O_A$ and $n'$ copies of $O_B$ for $A$ and $B$ respectively. The adversary can call them by calling $O_A[i]$ and $O_B[i']$ respectively. In a session that runs as expected, the adversary first calls $O_A[i]$. Then $O_A$ creates a fresh key $x'_k$ ($T_k$ is assumed to be a fixed-length type), encrypts it under $x_k$ with random coins $x_r$, computes the MAC under $x_{mk}$ of the ciphertext, and returns the ciphertext and the MAC. The function $k2b : T_k \to \text{bitstring}$ is the natural injection $k2b(x) = x$; it is needed only for type conversion. The adversary is then expected to forward this returned message to $O_B[i]$. When $O_B$ receives this message, it verifies the MAC, decrypts, and stores the obtained key in $x''_k$. (The function $i_{\perp} : \text{bitstring} \to \text{bitstring}_{\perp}$ is the natural injection; it is useful to check that decryption succeeded.) This key $x''_k$ should be secret.
The adversary is responsible for forwarding messages from *A* to *B*. It can call the oracles in unexpected ways in order to mount an attack.

This very small example is sufficient to illustrate the main features of CryptoVerif.

## 2.3 Type System

We use a type system to check that bitstrings of the proper type are passed to each function and oracle, and that array indices are used correctly.

To be able to type variable accesses used not under their definition (such accesses are guarded by a find construct) and oracle calls, the type-checking builds a type environment $\mathcal{E}$, which maps:

* variable names $x$ to types $[1, n_1] \times \dots \times [1, n_m] \to T$, where the definition of $x[i_1, \dots, i_m]$ of type $T$ occurs under replications or find that bind $i_1, \dots, i_m$ with declaration $i_j \le n_j$;

* oracle names $O$ to types $[1, n_1] \times \dots \times [1, n_m] \to T \to T'$, where the definition of $O[i_1, \dots, i_m](p) := P$ of type $T \to T'$ occurs under replications or find that bind $i_1, \dots, i_m$ with declaration $i_j \le n_j$.

For instance, the definition of $x[i_1, \dots, i_m]$ occurs under **foreach** $i_1 \le n_1$ **do**, ..., **foreach** $i_m \le n_m$ **do** or it occurs in the condition of **find** $u_1 = i_1 \le n_1, \dots, u_m = i_m \le n_m$ under no replication. The type $T$ is the one given in the definition of $x$ in $x[i] \stackrel{R}{\leftarrow} T$ or in a pattern $x[i] : T$ in an assignment, an oracle call, an oracle declaration, or a **get**. In the **find** construct, **find**...$x[i] = i \le n$, the type $T$ of $x$ is $T = [1, n]$. In the oracle call **let** $p = O[M_1, \dots, M_l, ?u_1[i] \le n_1, \dots, ?u_m[i] \le n_m](N)$ in $P$ **else** $P'$, the type $T_j$ of $u_j$ is $[1, n_j]$ for $j \le m$. The tool checks that all definitions of the same variable $x$ yield the same value of $\mathcal{E}(x)$, so that $\mathcal{E}$ is properly defined. Similarly, all definitions of the same oracle $O$ must yield the same value of $\mathcal{E}(O)$. While the type of variables can be determined by a preliminary pass on their definitions, provided their type is explicit at their definition, determining the type of oracles requires typing the oracle bodies. The type environment for oracles would then not be fully known at the beginning, but determined during typing by collecting constraints on the type of each oracle, provided the pattern in which the result of an oracle call is stored is explicitly typed. However, as we explain below, CryptoVerif currently does not accept oracle calls in its input language, which simplifies the typing algorithm. We sketch this algorithm below.

Oracles are typechecked in the type environment $\mathcal{E}$ using the rules of Figures 2, 3, and 4. These figures defines four judgments:

* $\mathcal{E} \vdash M : T$ means that the term $M$ has type $T$ in environment $\mathcal{E}$.

* $\mathcal{E} \vdash p : T$ means that the pattern $p$ has type $T$ in environment $\mathcal{E}$.

* $\mathcal{E} \vdash P : T$ means that the oracle body $P$ will return a value of type $T$ in environment $\mathcal{E}$.

* $\mathcal{E} \vdash Q$ means that the oracle definition $Q$ is well-typed in environment $\mathcal{E}$.

When a term $M$ never evaluates to a value (it always ends with **event_abort** $e$), it has the special type *any*, which can be converted to any other type by subtyping. Similarly, when an oracle body $P$ never returns (it always ends with **yield** or **event_abort** $e$), it has type *any*. The type *any* is not allowed in declarations of function symbols, tables, and events. Variables can have type *any* only when they are actually never defined (their definition is a term that always aborts). Patterns can have type *any* only when the pattern-matching will always fail (because it is an equality with a term that always aborts). The result type of oracles can be *any*, when they never return.
Typing rules for terms:

$$ \frac{\mathcal{E}(i) = T}{\mathcal{E} \vdash i : T} \qquad (TIndex) $$

$$ \frac{\mathcal{E}(x) = T_1 \times \dots \times T_m \to T \quad \forall j \le m, \mathcal{E} \vdash M_j : T_j}{\mathcal{E} \vdash x[M_1, \dots, M_m] : T} \qquad (TVar) $$

$$ \frac{f : T_1 \times \dots \times T_m \to T \quad \forall j \le m, \mathcal{E} \vdash M_j : T_j}{\mathcal{E} \vdash f(M_1, \dots, M_m) : T} \qquad (TFun) $$

$$ \frac{T \text{ fixed, bounded, or nonuniform} \quad \mathcal{E} \vdash x[\tilde{i}] : T \quad \mathcal{E} \vdash N : T'}{\mathcal{E} \vdash x[\tilde{i}] \stackrel{R}{\leftarrow} T; N : T'} \qquad (TNewT) $$

$$ \frac{\mathcal{E} \vdash M : T \quad \mathcal{E} \vdash p : T \quad \mathcal{E} \vdash N : T' \quad \mathcal{E} \vdash N' : T'}{\mathcal{E} \vdash \text{let } p = M \text{ in } N \text{ else } N' : T'} \qquad (TLetT) $$

$$ \frac{\mathcal{E} \vdash M : T \quad \mathcal{E} \vdash x[\tilde{i}] : T \quad \mathcal{E} \vdash N : T'}{\mathcal{E} \vdash \text{let } x[\tilde{i}] : T = M \text{ in } N : T'} \qquad (TLetT2) $$

$$ \frac{\mathcal{E} \vdash M : \mathit{bool} \quad \mathcal{E} \vdash N : T \quad \mathcal{E} \vdash N' : T}{\mathcal{E} \vdash \text{if } M \text{ then } N \text{ else } N' : T} \qquad (TIfT) $$

$$ \forall j \le m, \forall k \le m_j, \mathcal{E} \vdash u_{jk}[\tilde{i}] : [1, n_{jk}] $$

$$ \forall j \le m, \forall k \le l_j, \mathcal{E}[i_{j1} \mapsto [1, n_{j1}], \dots, i_{jm_j} \mapsto [1, n_{jm_j}]] \vdash M_{jk} : T_{jk} $$

$$ \forall j \le m, \mathcal{E}[i_{j1} \mapsto [1, n_{j1}], \dots, i_{jm_j} \mapsto [1, n_{jm_j}]] \vdash M_j : \mathit{bool} $$

$$ \forall j \le m, \mathcal{E} \vdash N_j : T \quad \mathcal{E} \vdash N : T $$

$$ \frac{\mathcal{E} \vdash \text{find}[\text{unique?}] (\bigoplus_{j=1}^m u_{j1}[\tilde{i}] = i_{j1} \le n_{j1}, \dots, u_{jm_j}[\tilde{i}] = i_{jm_j} \le n_{jm_j} \text{ suchthat defined}(M_{j1}, \dots, M_{jl_j}) \land M_j \text{ then } N_j) \text{ else } N : T}{\text{get}[\text{unique?}] \text{ Tbl}(p_1, \dots, p_l) \text{ suchthat } M \text{ in } N \text{ else } N' : T} \qquad (TFindT) $$

$$ \frac{\text{Tbl} : T_1 \times \dots \times T_l \quad \forall j \le l, \mathcal{E} \vdash M_j : T_j \quad \mathcal{E} \vdash N : T}{\mathcal{E} \vdash \text{insert } \text{Tbl}(M_1, \dots, M_l); N : T} \qquad (TInsertT) $$

$$ \frac{\text{Tbl} : T_1 \times \dots \times T_l \quad \forall j \le l, \mathcal{E} \vdash p_j : T_j \quad \mathcal{E} \vdash M : \mathit{bool} \quad \mathcal{E} \vdash N : T \quad \mathcal{E} \vdash N' : T}{\text{get}[\text{unique?}] \text{ Tbl}(p_1, \dots, p_l) \text{ suchthat } M \text{ in } N \text{ else } N' : T} \qquad (TGetT) $$

$$ \frac{e : T_1 \times \dots \times T_l \quad \forall j \le l, \mathcal{E} \vdash M_j : T_j \quad \mathcal{E} \vdash N : T}{\mathcal{E} \vdash \text{event } e(M_1, \dots, M_l); N : T} \qquad (TEventT) $$

$$ \frac{e : (\quad)}{\mathcal{E} \vdash \text{event_abort } e : \text{any}} \qquad (TEventAbortT) $$

$$ \frac{\mathcal{E} \vdash M : \mathit{any}}{\mathcal{E} \vdash M : T} \qquad (SubtypingT) $$

Typing rules for patterns:

$$ \frac{\mathcal{E} \vdash x[\tilde{i}] : T}{\mathcal{E} \vdash (x[\tilde{i}] : T) : T} \qquad (TVarP) $$

$$ \frac{f : T_1 \times \dots \times T_m \to T \quad \forall j \le m, \mathcal{E} \vdash p_j : T_j}{\mathcal{E} \vdash f(p_1, \dots, p_m) : T} \qquad (TFunP) $$

$$ \frac{\mathcal{E} \vdash M : T}{\mathcal{E} \vdash = M : T} \qquad (TEqP) $$

<caption>Figure 2: Typing rules (1)</caption>
Typing rules for oracle definitions:

$$ \mathcal{E} \vdash 0 \qquad (\text{TNil}) $$

$$ \frac{\mathcal{E} \vdash Q \qquad \mathcal{E} \vdash Q'}{\mathcal{E} \vdash Q | Q'} \qquad (\text{TPar}) $$

$$ \frac{\mathcal{E}[i \mapsto [1, n]] \vdash Q}{\mathcal{E} \vdash \text{foreach } i \le n \text{ do } Q} \qquad (\text{TRepl}) $$

$$ \frac{\mathcal{E}[O \mapsto T_1 \times \dots \times T_m \to T \to T'] \vdash Q}{\mathcal{E} \vdash \text{newOracle } O; Q} \qquad (\text{TNewOracle}) $$

$$ \frac{\mathcal{E} \vdash p : T \qquad \mathcal{E} \vdash P : T' \qquad \forall j \le m, \mathcal{E} \vdash i_j : T_j \qquad \mathcal{E}(O) = T_1 \times \dots \times T_m \to T \to T' \qquad \mathcal{E} \vdash O[i_1, \dots, i_m](p) := P}{\mathcal{E} \vdash p : T} \qquad (\text{TODecl}) $$

<caption>Figure 3: Typing rules (2)</caption>

In $x[M_1, \dots, M_m]$, $M_1, \dots, M_m$ must be of the suitable interval type. When $f(M_1, \dots, M_m)$ is called and $f: T_1 \times \dots \times T_m \to T$, $M_j$ must be of type $T_j$, and $f(M_1, \dots, M_m)$ is then of type $T$.

The term $x[\tilde{i}] \stackrel{R}{\leftarrow} T$; $N$ is accepted only when $T$ is declared fixed, bounded, or nonuniform. We check that $x[\tilde{i}]$ is of type $T$ (which is in fact always true when the construction of $\mathcal{E}$ succeeds). $N$ must well-typed, and its type is also the type of $x[\tilde{i}] \stackrel{R}{\leftarrow} T$; $N$.

In let $p = M$ in $N$ else $N'$, $p$ must have the same type as $M$, and $N$ and $N'$ must have the same type, which is also the type of let $p = M$ in $N$ else $N'$. The typing rules for patterns $p$ are found at the bottom of Figure 2. The pattern $x[\tilde{i}] : T$ has type $T$, provided $x[\tilde{i}]$ has type $T$ (which is in fact always true when the construction of $\mathcal{E}$ succeeds). The other typing rules for patterns are straightforward. The particular case let $x[\tilde{i}] : T = M$ in $N$ is typed similarly, except that the else branch is omitted.

In if $M$ then $N$ else $N'$, $M$ must be of type `bool` and $N$ and $N'$ must have the same type, which is also the type of if $M$ then $N$ else $N'$.

In

$$ \texttt{find}[\texttt{unique?}] (\bigoplus_{j=1}^m u_{j1}[\tilde{i}] = i_{j1} \le n_{j1}, \dots, u_{jm_j}[\tilde{i}] = i_{jm_j} \le n_{jm_j} \text{ suchthat} \\ \texttt{defined}(M_{j1}, \dots, M_{jl_j}) \land M_j \text{ then } N_j) \text{ else } N $$

the replication indices $i_{j1}, \dots, i_{jm_j}$ are bound in $M_{j1}, \dots, M_{jl_j}, M_j$, of types $[1, n_{j1}], \dots, [1, n_{jm_j}]$ respectively; $M_j$ is of type `bool` for all $j \le m$; $N_j$ for all $j \le m$ and $N$ all have the same type, which is also the type of the find term.

In `insert Tbl(M_1, \dots, M_l); N, M_1, \dots, M_l` must be of the type declared for the elements of the table `Tbl`, and the type of $N$ is the type of the `insert` term.

In `get[unique?] Tbl(p_1, \dots, p_l)` suchthat $M$ in $N$ else $N'$, $p_1, \dots, p_l$ must be of the type declared for the elements of the table `Tbl` and $M$ must be of type `bool`. The terms $N$ and $N'$ must have the same type, which is also the type of the `get` term.

In `event e(M_1, \dots, M_l); N, M_1, \dots, M_l` must be of the type declared for the arguments of event $e$, and the type of $N$ is the type of the `event` term.

The term `event_abort e` is of type `any`, and can thus be of any type (because it aborts the game); the event $e$ must be declared without argument, which we denote by `e: ()`. Terms of type
Typing rules for oracle bodies:

$$ \frac{\mathcal{E} \vdash N : T \qquad \mathcal{E} \vdash Q}{\mathcal{E} \vdash \text{ return } (N); Q : T} \qquad (\text{TRet}) $$

$$ \frac{\forall j \le l, \mathcal{E} \vdash M_j : T'_j \quad \forall j \le m, \mathcal{E} \vdash u_j[\tilde{i}] : [1, n_j] \quad \mathcal{E} \vdash N : T \quad \mathcal{E} \vdash p : T' \quad \mathcal{E} \vdash P : T'' \quad \mathcal{E} \vdash P' : T''}{\mathcal{E} \vdash O : T'_1 \times \dots \times T'_j \times [1, n_1] \times \dots \times [1, n_m] \to T \to T'} \qquad (\text{TCall}) $$

$$ \frac{\mathcal{E} \vdash \text{ let } p = O[M_1, \dots, M_l, ?u_1[\tilde{i}] \le n_1, \dots, ?u_m[\tilde{i}] \le n_m](N) \text{ in } P \text{ else } P' : T''}{T \text{ fixed, bounded, or nonuniform} \quad \mathcal{E} \vdash x[\tilde{i}] : T \quad \mathcal{E} \vdash P : T'} \qquad (\text{TNew}) $$

$$ \frac{\mathcal{E} \vdash x[\tilde{i}] \stackrel{R}{\leftarrow} T; P : T'}{\mathcal{E} \vdash M : T \quad \mathcal{E} \vdash p : T \quad \mathcal{E} \vdash P : T' \quad \mathcal{E} \vdash P' : T'} \qquad (\text{TLet}) $$

$$ \frac{\mathcal{E} \vdash M : T \quad \mathcal{E} \vdash p : T \quad \mathcal{E} \vdash P : T' \quad \mathcal{E} \vdash P' : T'}{\mathcal{E} \vdash \text{ let } p = M \text{ in } P \text{ else } P' : T'} \qquad (\text{TIf}) $$

$$ \frac{\mathcal{E} \vdash M : \mathit{bool} \quad \mathcal{E} \vdash P : T \quad \mathcal{E} \vdash P' : T}{\mathcal{E} \vdash \text{ if } M \text{ then } P \text{ else } P' : T} \qquad (\text{TIf}) $$

$$ \frac{\forall j \le m, \forall k \le m_j, \mathcal{E} \vdash u_{jk}[\tilde{i}] : [1, n_{jk}] \quad \forall j \le m, \forall k \le l_j, \mathcal{E}[i_{j1} \mapsto [1, n_{j1}], \dots, i_{jm_j} \mapsto [1, n_{jm_j}]] \vdash M_{jk} : T_{jk} \quad \forall j \le m, \mathcal{E}[i_{j1} \mapsto [1, n_{j1}], \dots, i_{jm_j} \mapsto [1, n_{jm_j}]] \vdash M_j : \mathit{bool} \quad \forall j \le m, \mathcal{E} \vdash P_j : T \quad \mathcal{E} \vdash P : T}{\mathcal{E} \vdash \text{ find}[\mathit{unique?}] \left( \bigoplus_{j=1}^m u_{j1}[\tilde{i}] = i_{j1} \le n_{j1}, \dots, u_{jm_j}[\tilde{i}] = i_{jm_j} \le n_{jm_j} \text{ suchthat } \mathit{defined}(M_{j1}, \dots, M_{j_l}) \wedge M_j \text{ then } P_j \right) \text{ else } P : T} \qquad (\text{TFind}) $$

$$ \frac{\mathcal{E} \vdash \text{ find}[\mathit{unique?}] \left( \bigoplus_{j=1}^m u_{j1}[\tilde{i}] = i_{j1} \le n_{j1}, \dots, u_{jm_j}[\tilde{i}] = i_{jm_j} \le n_{jm_j} \text{ suchthat } \mathit{defined}(M_{j1}, \dots, M_{j_l}) \wedge M_j \text{ then } P_j \right) \text{ else } P : T}{\mathcal{E} \vdash \text{ insert } \mathit{Tbl}(M_1, \dots, M_l); P : T} \qquad (\text{TInsert}) $$

$$ \frac{\mathcal{E} \vdash \mathit{Tbl} : T_1 \times \dots \times T_l \quad \forall j \le l, \mathcal{E} \vdash M_j : T_j \quad \mathcal{E} \vdash P : T}{\mathcal{E} \vdash \text{ insert } \mathit{Tbl}(M_1, \dots, M_l); P : T} \qquad (\text{TInsert}) $$

$$ \frac{\mathcal{E} \vdash \mathit{Tbl} : T_1 \times \dots \times T_l \quad \forall j \le l, \mathcal{E} \vdash p_j : T_j \quad \mathcal{E} \vdash M : \mathit{bool} \quad \mathcal{E} \vdash P : T \quad \mathcal{E} \vdash P' : T}{\text{get}[\mathit{unique?}] \ \mathit{Tbl}(p_1, \dots, p_l) \ \text{suchthat} \ M \text{ in } P \text{ else } P' : T} \qquad (\text{TGet}) $$

$$ \frac{e : T_1 \times \dots \times T_l \quad \forall j \le l, \mathcal{E} \vdash M_j : T_j \quad \mathcal{E} \vdash P : T}{\mathcal{E} \vdash \text{ event } e(M_1, \dots, M_l); P : T} \qquad (\text{TEvent}) $$

$$ \frac{e : ()}{\mathcal{E} \vdash \text{ event_abort } e : \mathit{any}} \qquad (\text{TEventAbort}) $$

$$ \mathcal{E} \vdash \text{ yield } : \mathit{any} \qquad (\text{TYield}) $$

$$ \frac{\mathcal{E} \vdash P : \mathit{any}}{\mathcal{E} \vdash P : T} \qquad (\text{Subtyping}) $$

$$ \frac{\mathcal{E}(O) = T_1 \times \dots \times T_m \to T \to T'}{\mathcal{E} \vdash O : T_1 \times \dots \times T_m \to T \to T'} \qquad (\text{TO}) $$

$$ \frac{\mathcal{E} \vdash O : T_1 \times \dots \times T_m \to T \to \mathit{any}}{\mathcal{E} \vdash O : T_1 \times \dots \times T_m \to T \to T'} \qquad (\text{SubtypingO}) $$

<caption>Figure 4: Typing rules (3)</caption>
any can then be given any type through the subtyping rule.

The type system for oracle definitions and bodies requires each subterm to be well-typed. In **foreach** $i \le n$ **do** *Q*, *i* is of type `[1, n]` in *Q*. The oracle commands $\leftarrow^R$, **let**, **if**, **find**, **insert**, **get**, **event**, and **event_abort** are typed similarly to the corresponding terms. The command **yield**, which aborts the execution of an oracle without returning any value, is typed with *any*. A **return** (*N*) is typed with the type of the term *N*. In an oracle call let *p* = *O*[*M*₁, ..., *M*ᵢ, ?*u*₁[*i*] ≤ *n*₁, ..., ?*u*ₘ[*i*] ≤ *n*ₘ](*N*) in *P* **else** *P*', the indices *M*₁, ..., *M*ᵢ, ?*u*₁[*i*] ≤ *n*₁, ..., ?*u*ₘ[*i*] ≤ *n*ₘ must have the same type as the indices at the definition of oracle *O*, the type of *N* must correspond to the type expected by the oracle *O*, the type of the result of oracle *O* must correspond to the type of the pattern *p*, and both branches *P* and *P*' must have the same type, which is also the type of the whole oracle call construct. Subtyping is lifted from terms to oracles with dedicated rules, and can be used either on an oracle body or an oracle definition.

We say that an occurrence of a term *M* in an oracle definition *Q* is of type *T* when *E* **†** *M* : *T* where *E* is the type environment of *Q* extended with *i* ↦→ [1, *n*) for each replication **foreach** *i* ≤ *n* **do** above *M* in *Q* and with *i*<sub>j1</sub> ↦→ [1, *n*<sub>j1</sub>], ..., *i*<sub>jm<sub>j</sub></sub> ↦→ [1, *n*<sub>jm<sub>j</sub></sub>] for each **find**[unique?](⊕<sub>j=1</sub><sup>*m*</sup> *u*<sub>j1</sub>[*i*] = *i*<sub>j1</sub> ≤ *n*<sub>j1</sub>, ..., *u*<sub>jm<sub>j</sub></sub>[*i*] = *i*<sub>jm<sub>j</sub></sub> ≤ *n*<sub>jm<sub>j</sub></sub> **such that** defined(*M*<sub>j1</sub>, ..., *M*<sub>jl<sub>j</sub></sub>) ∧ *M*<sub>j</sub> then *P*<sub>j</sub>) **else** *P* such that the considered occurrence of *M* is in the condition defined(*M*<sub>j1</sub>, ..., *M*<sub>jl<sub>j</sub></sub>) ∧ *M*<sub>j</sub>.

**Invariant 8 (Typing)** The oracle definition $Q_0$ satisfies Invariant 8 if and only if there exists a type environment $\mathcal{E}$ for $Q_0$ such that $\mathcal{E} \vdash Q_0$.

On the implementation side, we only have to check that input processes following the subset
for the initial game (see Figure 13) are well-typed, so we do not need to deal with oracle calls and
**newOracle.** In practice, the type of oracles in the type environment is determined by maintaining
a list of oracles when going through the process, storing for each oracle its name, the type of
indices, the type of arguments, and the potential type of the returns. For distinct branches of
execution, we merge the oracle lists allowing duplicated names but ensuring that the same oracle
name always corresponds to the same number of indices, the same type of arguments, and that
the return type either corresponds to none or the same. For parallel execution branches and
for oracles defined syntactically one under the other, we forbid oracles with the same names, to
guarantee Invariant 7.

The type of variables in the type environment is determined by inspecting all variables def-
initions in a preliminary pass before the actual typing. Variables with several incompatible
definitions (different indices, different types, or variables defined in the same branch of a test,
which would contradict Invariant 1) are automatically renamed to distinct variable names. Such
variables cannot be used queries and nor in defined conditions of find. For simplicity, variables
defined without giving them an explicit type also cannot be used in queries and nor in defined
conditions of find, even if their type is later inferred by the typing algorithm, and are also renamed
to distinct variable names.

Looking forward, an adversary against a protocol will be made of two components:

* an attacker *A* that can be instantiated by any black-box interactive and stateful function;

* an adversary context *C*, inside our game syntax, that allows the adversary to, e.g., raise events.

We require the adversary context to be well-typed. This requirement does not restrict its com-
puting power, because it can always define type-cast functions $f : T \to T'$ to bypass the type
system. Similarly, the type system does not restrict the class of protocols that we consider, since
the protocol may contain type-cast functions. The type system just makes explicit which set of
values may appear at each point of the protocol.

The attacker calls to oracles will also be well-typed by the semantics, which once again does
not restrict its computing power.

2.4 Formal Semantics

2.4.1 Definition of the Semantics

The formal semantics of our programming language is presented in Figures 5, 6, 8, 9, 10, and 11.

In this semantics, each term *M* or process *P* or *Q* is labeled by a program point *μ*, replacing *M* with *μ*^*M* and similarly for *P* and *Q*. We still use the notations *M*, *P*, *Q* for terms and processes tagged with program points. The program points are used in order to track from where each term or process comes from in the initial oracle definition. These program points are simply constant tags, and the initial oracle definition is tagged with a distinct program point at each subterm and subprocess.

The semantics depends on an attacker that may interact with the oracles. We consider
attackers $\mathcal{A}$ from a recursively defined attacker space $\mathcal{BB}$, that are probabilistic functions of type
$\mathcal{A} : \text{Bitstring} \mapsto \text{Distr}(\mathcal{BB} \times \text{Bitstring})$. To each input, the attacker $\mathcal{A}$ gives out a distribution
yielding the corresponding output and next attacker step with some probability. It models an
interactive black-box attacker, where given an input, it gives back with some probability both an
output and the next attacker step. Here, $\text{Bitstring} = \{0,1\}^*$ is the set of concrete bitstrings, and
we implicitly rely on the efficient bijections from types and oracle names to concrete bitstrings
so that the attacker can interact with the oracles.

A semantic configuration is a sextuple $E, St, Q, Or, T, \mu Ev$, where

* $E$ is an environment mapping array cells to values.

* $St$ is an execution stack of the form $(\sigma_0, P_0) :: \dots :: (\sigma_m, P_m) :: \mathcal{A}$ where $P_j$ are oracle bodies and $\sigma_j$ are the associated mapping sequences which give values of replication indices. The oracle body $P_0$ is the one currently being executed, and the oracle bodies $P_1, \dots, P_m$ correspond to oracle calls that have not returned yet. The stack always contains at least one pair $(\sigma_j, P_j)$ and always contains as a last element an attacker $\mathcal{A}$.

The mapping sequence $\sigma = [i_1 \mapsto a_1, \dots, i_m \mapsto a_m]$ is a sequence of mappings $i_j \mapsto a_j$, which can also be interpreted as a function: $\sigma(i_j) = a_j$ for all $j \le m$, and $\sigma(\tilde{i})$ is defined by the natural extension to sequences. However, using a sequence allows us to define $\text{Dom}(\sigma) = [i_1, \dots, i_m]$ to be the sequence of current replication indices and $\text{Im}(\sigma) = [a_1, \dots, a_m]$ to be the sequence of their values. When $\sigma = [i_1 \mapsto a_1, \dots, i_m \mapsto a_m]$, $\sigma[i_{m+1} \mapsto a_{m+1}, \dots, i_l \mapsto a_l] = [i_1 \mapsto a_1, \dots, i_l \mapsto a_l]$.

* $\mathcal{Q}$ is the multiset of oracle declarations running in parallel with $P$, with their associated mapping sequences giving values of replication indices. It is the set of callable oracles.

* $Or = (Or_{\text{pub}}, Or_{\text{priv}})$ represents the oracles already created. $Or_{\text{pub}}$ is the set of public oracles, which can be called by the adversary; $Or_{\text{priv}}$ is the set of private oracles.

* $\mathcal{T}$ defines the contents of tables. It is a list of $Tbl(a_1, \dots, a_m)$ indicating that table $Tbl$ contains the element $(a_1, \dots, a_m)$.

* $\mu Ev$ is a sequence representing the events executed so far. Each element of the sequence is of the form $(\mu, \tilde{a}) : e(a_1, \dots, a_m)$, meaning that the event $e(a_1, \dots, a_m)$ has been executed at program point $\mu$ with replication indices evaluating to $\tilde{a}$.
We define $\mathcal{E}v = \text{removepp}(\mu\mathcal{E}v) = [e(a_1, \dots, a_m) | (\mu, \tilde{a}) : e(a_1, \dots, a_m) \in \mu\mathcal{E}v]$ to be the sequence of events $\mu\mathcal{E}v$ without their associated program points and replication indices.

In addition to the grammar given in Figure 1, the terms $M$ of the semantics can be values $a$ and abort event values $\mathbf{event\_abort}(\mu, \tilde{a}) : e$, and the oracle bodies $P$ can be $\mathbf{abort}$, corresponding to the situation in which the game has been aborted. These additional terms and oracle bodies are not tagged with program points. (They do not occur in the initial oracle definition.)

The semantics is defined by reduction rules of the form $E, St, Q, Or, T, \mu\mathcal{E}v \xrightarrow{p} t E', St', Q', Or', T', \mu\mathcal{E}v'$ meaning that $E, St, Q, Or, T, \mu\mathcal{E}v$ reduces to $E', St', Q', Or', T', \mu\mathcal{E}v'$ with probability $p$. The index $t$ just serves in distinguishing reductions that yield the same configuration with the same probability in different ways, so that the probability of a certain reduction can be computed correctly:

$$ \Pr[E, St, Q, Or, T, \mu\mathcal{E}v \to E', St', Q', Or', T', \mu\mathcal{E}v'] = \sum_{E, St, Q, Or, T, \mu\mathcal{E}v \xrightarrow{p} t E', St', Q', Or', T', \mu\mathcal{E}v'} p $$

The probability of a trace $Tr = E_1, St_1, Q_1, Or_1, T_1, \mu\mathcal{E}v_1 \xrightarrow{p_1} t_1 \dots \xrightarrow{p_{m-1}} t_{m-1} E_m, St_m, Q_m, Or_m, T_m, \mu\mathcal{E}v_m$ is $\Pr[Tr] = p_1 \times \dots \times p_{m-1}$. We define the semantics only for patterns $x[\tilde{i}] : T$, the other patterns can be encoded as outlined in Section 2.1.

In Figures 5 and 6, we define an auxiliary relation for evaluating terms: $E, \sigma, M, T, \mu\mathcal{E}v \xrightarrow{p} t E', \sigma, M', T', \mu\mathcal{E}v'$ means that the term $M$ reduces to $M'$ in environment $E$ with the replication indices defined by $\sigma$, the table contents $T$, and the sequence of events $\mu\mathcal{E}v$, with probability $p$. Rule (RepIndex) evaluates replication indices using the function $\sigma$. Rule (Var) looks for the value of the variable in the environment $E$. Rule (Fun) evaluates the function call. Rule (NewT) chooses a random $a \in T$ according to distribution $D_T$, and stores it in $x[\sigma(\tilde{i})]$ by extending the environment $E$ accordingly. Similarly, Rule (LetT) extends the environment $E$ with the value of $x[\sigma(\tilde{i})]$. Rule (IfT1) evaluates the then branch of if when the condition is true, and Rule (IfT2) evaluates the else branch otherwise.

Rules (FindTE) to (FindT3) define the semantics of find. First, they all evaluate the conditions for all branches $j$ and all values of the indices $i_{j1}, \dots, i_{jm_j}$. If one of these evaluations executes an event (which can happen in case the condition contains an $\mathbf{event\_abort}$ $e$ or a $\mathbf{find}$[$\mathbf{unique}_e$]), the whole find executes the same event; in case the evaluations of the conditions execute several different events, one of them is chosen randomly, according to distribution $D_{\mathbf{find}}(S)$, that is, almost uniformly over the choices of branches and indices (Rule (FindTE)). Otherwise, the branch and indices for which the condition is true are collected in a set $S$. If $S$ is empty, the else branch of the find is executed (Rule (FindT2)). When $S$ is not empty, two cases can happen. Either the find is not marked [$\mathbf{unique}_e$], and we choose an element $v_0 = (j', a'_1, \dots, a'_{m_{j'}})$ of $S$ randomly according to the distribution $D_{\mathbf{find}}(S)$, store the corresponding indices $a'_1, \dots, a'_{m_{j'}}$ in $u_{j'1}[\sigma(\tilde{i})], \dots, u_{j'm_{j'}}[\sigma(\tilde{i})]$ by extending the environment accordingly, and we continue with the selected branch $N'_j$. If the find is marked [$\mathbf{unique}_e$] and $S$ has a single element, we do the same. If the find is marked [$\mathbf{unique}_e$] and $S$ has several elements, we execute the event $e$ (Rule (FindT3)). We recall that $D_{\mathbf{find}}(S)(v_0)$ denotes the probability of choosing $v_0$ in the distribution $D_{\mathbf{find}}(S)$. The terms in conditions of find may define variables, included in the environment $E''$; we ignore these additional variables and compute the final environment from the initial environment $E$, because these variables have no array accesses by Invariant 3, so the values of these variables are not used after the evaluation of the condition. The conditions of find, $D \wedge M$, are evaluated using Rules (DefinedNo) and (DefinedYes). If an element of the defined condition $D$ is not defined, then the condition is false (Rule (DefinedNo)); when all elements of the defined condition are defined, we evaluate $M$ (Rule (DefinedYes)). Since terms in conditions of find do not contain
$$E, \sigma, \mu^i, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{1} E, \sigma, \sigma(i), \mathcal{T}, \mu\mathcal{E}v \quad \text{(ReplIndex)}$$

$$\frac{x[a_1, \dots, a_m] \in \text{Dom}(E)}{} \quad \text{(Var)}$$

$$E, \sigma, \mu^x [a_1, \dots, a_m], \mathcal{T}, \mu\mathcal{E}v \xrightarrow{1} E, \sigma, E(x[a_1, \dots, a_m]), \mathcal{T}, \mu\mathcal{E}v$$

$$\frac{f : T_1 \times \dots \times T_m \to T \quad \forall j \le m, a_j \in T_j \quad f(a_1, \dots, a_m) = a}{E, \sigma, \mu^f(a_1, \dots, a_m), \mathcal{T}, \mu\mathcal{E}v \xrightarrow{1} E, \sigma, a, \mathcal{T}, \mu\mathcal{E}v} \quad \text{(Fun)}$$

$$\frac{a \in T \quad E' = E[x[\sigma(\tilde{i})] \mapsto a]}{E, \sigma, \mu^x [\tilde{i}] \stackrel{R}{\leftarrow} T; N, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{D_{\mathcal{T}}(a)} N(a) \quad E', \sigma, N, \mathcal{T}, \mu\mathcal{E}v} \quad \text{(NewT)}$$

$$\frac{a \in T \quad E' = E[x[\sigma(\tilde{i})] \mapsto a]}{E, \sigma, \mu^l \text{let } x[\tilde{i}] : T = a \text{ in } N, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{1} E', \sigma, N, \mathcal{T}, \mu\mathcal{E}v} \quad \text{(LetT)}$$

$$E, \sigma, \mu^l \text{if true then } N \text{ else } N', \mathcal{T}, \mu\mathcal{E}v \xrightarrow{1} E, \sigma, N, \mathcal{T}, \mu\mathcal{E}v \quad \text{(IfT1)}$$

$$\frac{a \neq \text{true}}{E, \sigma, \mu^l \text{if a then } N \text{ else } N', \mathcal{T}, \mu\mathcal{E}v \xrightarrow{1} E, \sigma, N', \mathcal{T}, \mu\mathcal{E}v} \quad \text{(IfT2)}$$

$(v_k)_{1 \le k \le l}$ is the sequence of $(j, a_1, \dots, a_{m_j})$ for $a_1 \in [1, n_{j1}], \dots, a_{m_j} \in [1, n_{jm_j}]$

ordered in increasing lexicographic order

$$\forall k \in [1, l], E, \sigma[i_{j1} \mapsto a_1, \dots, i_{jm_j} \mapsto a_{mj}], D_j \wedge M_j, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p_k} t_k E_k, \sigma_k, r_k, \mathcal{T}, \mu\mathcal{E}v$$

where $v_k = (j, a_1, \dots, a_{m_j})$ and $r_k$ is a value or `event_abort` $(\mu', \tilde{a}) : e$

$$S = \{k \mid \exists(\mu', \tilde{a}, e), r_k = \text{event_abort}(\mu', \tilde{a}) : e\} \quad k_0 \in S$$

$$E, \sigma, \mu^l \text{find}[\text{unique?}] (\bigoplus_{j=1}^m u_{j1}[\tilde{i}] = i_{j1} \le n_{j1}, \dots, u_{jm_j}[\tilde{i}] = i_{jm_j} \le n_{jm_j} \text{ suchthat}$$

$$D_j \wedge M_j \text{ then } N_j) \text{ else } N, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p_1 \dots p_l D_{\text{find}}(S)(k_0)} t_{1 \dots t_l F E(k_0)} E_{k_0}, \sigma_{k_0}, r_{k_0}, \mathcal{T}, \mu\mathcal{E}v \quad \text{(FindTE)}$$

$(v_k)_{1 \le k \le l}$ is the sequence of $(j, a_1, \dots, a_{m_j})$ for $a_1 \in [1, n_{j1}], \dots, a_{m_j} \in [1, n_{jm_j}]$

ordered in increasing lexicographic order

$$\forall k \in [1, l], E, \sigma[i_{j1} \mapsto a_1, \dots, i_{jm_j} \mapsto a_{mj}], D_j \wedge M_j, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p_k} t_k E''(\sigma'), \sigma', r_k, \mathcal{T}, \mu\mathcal{E}v$$

where $v_k = (j, a_1, \dots, a_{m_j})$ and $r_k$ is a value

$$S = \{v_k \mid r_k = \text{true}\} \quad |S| = 1 \text{ or } [\text{unique?}] \text{ is empty}$$

$$v_0 = (j', a'_1, \dots, a'_{m'_{j'}}) \in S \quad E' = E[u_{j'1}[\sigma(\tilde{i})] \mapsto a'_1, \dots, u_{j'm'_{j'}}[\sigma(\tilde{i})] \mapsto a'_{m'_{j'}}]$$

$$E, \sigma, \mu^l \text{find}[\text{unique?}] (\bigoplus_{j=1}^m u_{j1}[\tilde{i}] = i_{j1} \le n_{j1}, \dots, u_{jm_j}[\tilde{i}] = i_{jm_j} \le n_{jm_j} \text{ suchthat}$$

$$D_j \wedge M_j \text{ then } N_j) \text{ else } N, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p_1 \dots p_l D_{\text{find}}(S)(v_0)} t_{1 \dots t_l F_1(v_0)} E', \sigma, N_{j'}, \mathcal{T}, \mu\mathcal{E}v \quad \text{(FindT1)}$$

First four lines as in (FindT1) \quad $S = \{v_k \mid r_k = \text{true}\} = \emptyset$

$$\frac{E, \sigma, \mu^l \text{find}[\text{unique?}] (\bigoplus_{j=1}^m u_{j1}[\tilde{i}] = i_{j1} \le n_{j1}, \dots, u_{jm_j}[\tilde{i}] = i_{jm_j} \le n_{jm_j} \text{ suchthat} \quad D_j \wedge M_j \text{ then } N_j) \text{ else } N, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p_1 \dots p_l} t_{1 \dots t_l F_2} E, \sigma, N, \mathcal{T}, \mu\mathcal{E}v}{S = \{v_k \mid r_k = \text{true}\} \quad |S| > 1} \quad \text{(FindT2)}$$

First four lines as in (FindT1) \quad $S = \{v_k \mid r_k = \text{true}\}$ \quad $|S| > 1$

$$E, \sigma, \mu^l \text{find}[\text{unique}_e] (\bigoplus_{j=1}^m u_{j1}[\tilde{i}] = i_{j1} \le n_{j1}, \dots, u_{jm_j}[\tilde{i}] = i_{jm_j} \le n_{jm_j} \text{ suchthat}$$

$$D_j \wedge M_j \text{ then } N_j) \text{ else } N, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p_1 \dots p_l} t_{1 \dots t_l F_3} E, \sigma, \text{event_abort}(\mu, \text{Im}(\sigma)) : e, \mathcal{T}, \mu\mathcal{E}v \quad \text{(FindT3)}$$

<caption>Figure 5: Semantics (1): terms, first part</caption>
$$E, \sigma, \mu^{\text{insert}} \Tbl(a_1, \dots, a_l); N, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{1} E, \sigma, N, (\mathcal{T}, \Tbl(a_1, \dots, a_l)), \mu\mathcal{E}v \quad \text{(InsertT)}$$

$$[v_1, \dots, v_m] = [x \in \mathcal{T} \mid \exists a_1, \dots, \exists a_l, x = \Tbl(a_1, \dots, a_l)]$$

$$\forall k \in [1, m], E[x_1[\sigma(\tilde{i})] \mapsto a_1, \dots, x_l[\sigma(\tilde{i})] \mapsto a_l], \sigma, M, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p_k} \mathcal{T}_{\tilde{k}} E_k, \sigma_k, r_k, \mathcal{T}, \mu\mathcal{E}v$$

$$\text{where } v_k = \Tbl(a_1, \dots, a_l) \text{ and } r_k \text{ is a value or } \text{event\_abort}(\mu', \tilde{a}) : e$$

$$S = \{k \in [1, m] \mid \exists(\mu', \tilde{a}, e), r_k = \text{event\_abort}(\mu', \tilde{a}) : e\} \quad k_0 \in S \quad \text{(GetTE)}$$

$$E, \sigma, \mu^{\text{get}[\text{unique?}]} \Tbl(x_1[\tilde{i}] : T_1, \dots, x_l[\tilde{i}] : T_l) \text{ suchthat } M \text{ in } N \text{ else } N', \mathcal{T}, \mu\mathcal{E}v$$

$$\xrightarrow{p_1 \dots p_m D_{\text{get}}(S)(k_0)} \mathcal{T}_{t_1 \dots t_m G E(k_0)} E_{k_0}, \sigma_{k_0}, r_{k_0}, \mathcal{T}, \mu\mathcal{E}v$$

$$[v_1, \dots, v_m] = [x \in \mathcal{T} \mid \exists a_1, \dots, \exists a_l, x = \Tbl(a_1, \dots, a_l)]$$

$$\forall k \in [1, m], E[x_1[\sigma(\tilde{i})] \mapsto a_1, \dots, x_l[\sigma(\tilde{i})] \mapsto a_l], \sigma, M, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p_k} \mathcal{T}'' E'', \sigma, r_k, \mathcal{T}, \mu\mathcal{E}v$$

$$\text{where } v_k = \Tbl(a_1, \dots, a_l) \text{ and } r_k \text{ is a value}$$

$$S = \{k \in [1, m] \mid r_k = \text{true}\}$$

$$|S| = 1 \text{ or } [\text{unique?}] \text{ is empty}$$

$$k_0 \in S \qquad \Tbl(a_1, \dots, a_l) = v_{k_0} \qquad E' = E[x_1[\sigma(\tilde{i})] \mapsto a_1, \dots, x_l[\sigma(\tilde{i})] \mapsto a_l] \quad \text{(GetT1)}$$

$$E, \sigma, \mu^{\text{get}[\text{unique?}]} \Tbl(x_1[\tilde{i}] : T_1, \dots, x_l[\tilde{i}] : T_l) \text{ suchthat } M \text{ in } N \text{ else } N', \mathcal{T}, \mu\mathcal{E}v$$

$$\xrightarrow{p_1 \dots p_m D_{\text{get}}(S)(k_0)} \mathcal{T}_{t_1 \dots t_m G_1(k_0)} E', \sigma, N, \mathcal{T}, \mu\mathcal{E}v$$

$$\text{First four lines as in (GetT1)} \qquad S = \emptyset \quad \text{(GetT2)}$$

$$E, \sigma, \mu^{\text{get}[\text{unique?}]} \Tbl(x_1[\tilde{i}] : T_1, \dots, x_l[\tilde{i}] : T_l) \text{ suchthat } M \text{ in } N \text{ else } N', \mathcal{T}, \mu\mathcal{E}v$$

$$\xrightarrow{p_1 \dots p_m} \mathcal{T}_{t_1 \dots t_m G_2} E, \sigma, N', \mathcal{T}, \mu\mathcal{E}v$$

$$\text{First four lines as in (GetT1)} \qquad |S| > 1 \quad \text{(GetT3)}$$

$$E, \sigma, \mu^{\text{get}[\text{unique}_e]} \Tbl(x_1[\tilde{i}] : T_1, \dots, x_l[\tilde{i}] : T_l) \text{ suchthat } M \text{ in } N \text{ else } N', \mathcal{T}, \mu\mathcal{E}v$$

$$\xrightarrow{p_1 \dots p_m} \mathcal{T}_{t_1 \dots t_m G_3} E, \sigma, \text{event\_abort}(\mu, \text{Im}(\sigma)) : e, \mathcal{T}, \mu\mathcal{E}v$$

$$E, \sigma, \mu^{\text{event}} e(a_1, \dots, a_l); N, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{1} E, \sigma, N, \mathcal{T}, (\mu\mathcal{E}v, (\mu, \text{Im}(\sigma)) : e(a_1, \dots, a_l)) \quad \text{(EventT)}$$

$$E, \sigma, \mu^{\text{event\_abort}} e, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{1} E, \sigma, \text{event\_abort}(\mu, \text{Im}(\sigma)) : e, \mathcal{T}, \mu\mathcal{E}v \quad \text{(EventAbortT)}$$

$$\frac{E, \sigma, N, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p} E', \sigma', N', \mathcal{T}', \mu\mathcal{E}v'}{E, \sigma, C[N], \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p} E', \sigma', C[N'], \mathcal{T}', \mu\mathcal{E}v'} \quad \text{(CtxT)}$$

$$E, \sigma, C[\text{event\_abort}(\mu, \tilde{a}) : e], \mathcal{T}, \mu\mathcal{E}v \xrightarrow{1} E, \sigma, \text{event\_abort}(\mu, \tilde{a}) : e, \mathcal{T}, \mu\mathcal{E}v \quad \text{(CtxEventT)}$$

$$\frac{\neg\forall j \le l, \exists a_j, E, \sigma, M_j, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{1^*} E, \sigma, a_j, \mathcal{T}, \mu\mathcal{E}v}{E, \sigma, \text{defined}(M_1, \dots, M_l) \wedge M, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{1} E, \sigma, \text{false}, \mathcal{T}, \mu\mathcal{E}v} \quad \text{(DefinedNo)}$$

$$\frac{\forall j \le l, \exists a_j, E, \sigma, M_j, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{1^*} E, \sigma, a_j, \mathcal{T}, \mu\mathcal{E}v}{E, \sigma, \text{defined}(M_1, \dots, M_l) \wedge M, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{1} E, \sigma, M, \mathcal{T}, \mu\mathcal{E}v} \quad \text{(DefinedYes)}$$

<caption>Figure 6: Semantics (2): terms, second part, and defined conditions</caption>
$$
\begin{align*}
C &::= \mu x[a_1, \dots, a_{k-1}, [], M_{k+1}, \dots, M_m] \\
  &\phantom{::=} \mu f(a_1, \dots, a_{k-1}, [], M_{k+1}, \dots, M_m) \\
  &\phantom{::=} \mu \text{let } x[\tilde{i}] : T = [] \text{ in } N \\
  &\phantom{::=} \mu \text{if } [] \text{ then } N \text{ else } N' \\
  &\phantom{::=} \mu \text{event } e(a_1, \dots, a_{k-1}, [], M_{k+1}, \dots, M_l); N \\
  &\phantom{::=} \mu \text{insert } Tbl(a_1, \dots, a_{k-1}, [], M_{k+1}, \dots, M_l); N
\end{align*}
$$

<caption>Figure 7: Term contexts</caption>

insert nor event (Invariant 4), the table contents and the sequence of events are left unchanged
by the evaluation of the condition of find.

Rule (InsertT) inserts the new table element in $\mathcal{T}$. Rules (GetTE) to (GetT3) define the semantics of get. We denote by $[x \in L | f(x)]$ the list of all elements $x$ of the list $L$ that satisfy $f(x)$, in the same order as in $L$. We denote by $|L|$ the length of list $L$. We denote by $\text{nth}(L, j)$ the $j$-th element of the list $L$. Rule (GetTE) executes `event_abort e` when the evaluation of the condition $M$ executes `event_abort e` for some element of the table `Tbl`; when several events may be executed, one of them is chosen randomly according to distribution $D_{\text{get}}(S)$, that is, almost uniformly in the elements of the table `Tbl`. Rules (GetT1), (GetT2), and (GetT3) compute the set $S$ of elements of indices of elements of table `Tbl` in $\mathcal{T}$ that satisfy condition $M$. If $S$ is empty, we execute $N'$ (Rule (GetT2)). When $S$ is not empty, two cases can happen. If the `get` is not marked `[unique_e]` or $S$ has a single element, then one of its elements is chosen randomly according to distribution $D_{\text{get}}(S)$, we store this element in $x_1[\sigma(\tilde{i})], \dots, x_l[\sigma(\tilde{i})]$ by extending the environment $E$, and continue by executing $N$ (Rule (GetT1)). If the `get` is marked `[unique_e]` and $S$ contains several elements, then we execute `event e` and abort (Rule (GetT3)). Since terms in conditions of `get` do not contain `insert` nor `event` (Invariant 4), the table contents and the sequence of events are left unchanged by the evaluation of $M$. The modified environment $E''$ obtained after evaluating a condition $M$ can be ignored because there are no array accesses to the variables defined in conditions of `get`, by Invariant 3, so the values of these variables are not used after the evaluation of the condition.

**Remark 1** Another way of defining the semantics of tables would be to consider two distinct calculi, one with tables (used for the initial game), and one without tables (used for the other games). The semantics of the calculus without tables can be defined without the component $\mathcal{T}$. We then need to relate the two semantics.

Rule (EventT) adds the executed event to $\mu\mathcal{E}v$. Rule (EventAbortT) executes `event_abort e`. The event $e$ is not immediately added to $\mu\mathcal{E}v$, because for terms that occur in conditions of find, in case several branches execute `event_abort`, we may need to choose randomly which event will be added to $\mu\mathcal{E}v$. Hence, we use the result `event_abort (\mu, \tilde{a}) : e` instead.

Rules (CtxT) and (CtxEventT) allow evaluating terms under a context. In these rules, $C$ is an elementary context, of one of the forms defined in Figure 7. When the term $N$ reduces to some other term $N'$, Rule (CtxT) allows one to reduce it in the same way under a context $C$. When the term $N$ is an event, $C[N]$ also executes the same event by Rule (CtxEventT).

These rules define a small-step semantics for terms. We consider the reflexive and transitive closure $\xrightarrow{p}^*$ of the relation $\xrightarrow{p}$ to reach directly the normal form of the term, which can be either a
$$ \{(\sigma, \mu^0)\} \uplus Q, Or \rightsquigarrow Q, Or \qquad (\text{Nil}) $$

$$ \{(\sigma, \mu(Q_1 | Q_2))\} \uplus Q, Or \rightsquigarrow \{(\sigma, Q_1), (\sigma, Q_2)\} \uplus Q, Or \qquad (\text{Par}) $$

$$ \{(\sigma, \mu \text{foreach } i \le n \text{ do } Q)\} \uplus Q, Or \rightsquigarrow \{(\sigma[i \mapsto a], Q) | a \in [1, n]\} \uplus Q, Or \qquad (\text{Repl}) $$

$$ Or = (Or_{\text{pub}}, Or_{\text{priv}}) \qquad O' \notin Or_{\text{pub}} \cup Or_{\text{priv}} \qquad \frac{\{(\sigma, \mu \text{newOracle } O; Q)\} \uplus Q, Or \rightsquigarrow \{(\sigma, Q\{O'/O\})\} \uplus Q, (Or_{\text{pub}}, Or_{\text{priv}} \cup \{O'\})}{(\text{NewOracle})} $$

$$ \{(\sigma, \mu O[\tilde{i}](x[\tilde{i}] : T) := P)\} \uplus Q, Or \rightsquigarrow \{(\sigma, \mu O[\sigma(\tilde{i})](x[\tilde{i}] : T) := P)\} \uplus Q, Or \qquad (\text{DefOracle}) $$

reduce(Q, Or) is the normal form of Q, Or by $\rightsquigarrow$

<caption>Figure 8: Semantics (3): oracle definitions</caption>

value *a* or an abort event value `event_abort` (*μ*, *ã*) : *e*. We have *E*, *σ*, *M*, *T*, *μEv* $\xrightarrow{1}^*$ *E*, *σ*, *M*, *T*, *μEv* and, if *E*, *σ*, *M*, *T*, *μEv* $\xrightarrow{p}$ *E*', *σ*', *M*', *T*', *μEv*' and *E*', *σ*', *M*', *T*', *μEv*' $\xrightarrow{p'}^*$ *E*'', *σ*'', *M*'', *T*'', *μEv*'', then *E*, *σ*, *M*, *T*, *μEv* $\xrightarrow{p \times p'}^*$ *E*'', *σ*'', *M*'', *T*'', *μEv*'': we take the product of the probabilities to have the probability of a sequence of reductions, and we specify which sequence was taken by a list of indices *t*, *t*'.

Figure 8 defines the semantics of oracle definitions. We use an auxiliary reduction relation $\rightsquigarrow$, for reducing oracle definitions. This relation transforms configurations of the form $Q, Or$. Rule (Nil) removes nil definitions. Rules (Par) and (Repl) expand parallel compositions and replications, respectively. Rule (NewOracle) creates a new oracle and adds it to $Or_{priv}$. Semantic configurations are considered equivalent modulo renaming of oracles in $Or_{priv}$, so that a single semantic configuration is obtained after applying (NewOracle). Rule (DefOracle) evaluates the replication indices in an oracle declaration. The oracle itself is not executed: the call is done by the (OracleCall) rule. The relation $\rightsquigarrow$ is convergent (confluent and terminating), so it has normal forms. Oracle definitions in $Q$ in configurations $E, St, Q, Or, T, μEv$ are always in normal form by $\rightsquigarrow$, so they always start with an oracle declaration.

Finally, Figures 9, 10, and 11 define the semantics of oracles bodies. Most of these rules are very similar to those for terms: they just use oracles instead of terms as continuations, and include a whole semantic configuration. Rule (EventAbort) executes event *e* and aborts the game, by reducing to the configuration with oracle body `abort`. Similarly to the case of terms, Rules (Ctx) and (CtxEvent) allow evaluating terms under a context inside an oracle body. In these rules, *C* is an elementary context, of one of the forms defined in Figure 12.

Rule (OracleCall) performs an oracle call: it selects an available oracle, and immediately executes it. (The oracle call blocks if no suitable oracle is available.) The head of the execution stack after this rule is the body of the called oracle. In this rule, *S* is a multiset. When we take probabilities over multisets, we consider that $D_{call}(S)(\sigma', Q_0)$ is the probability of choosing one of the elements equal to $\sigma'$, $Q_0$ in *S* according to the distribution $D_{call}(S)$, so that the probability of choosing any element equal to $(\sigma', Q_0)$ is in fact $S(\sigma', Q_0) \times D_{call}(S)(\sigma', Q_0)$.

The rule (Return) corresponds to an oracle body finishing its execution and returning the result to the caller, which is the next oracle $P_0$ in the execution stack. The oracle definitions that follow the return are added to the set of available oracles, after reducing them by rules of Figure 8. The in branch of the caller is then executed. The rule (Yield) corresponds to an oracle body finishing its execution by `yield`. The else branch of the caller is then executed.

Rule (AttIO) corresponds to the attacker receiving a return and then triggering a new oracle call. The probability is over all possible attacker choices, as well as the corresponding oracles.
Same assumption as in (FindTE) $r_{k_0} = \text{event_abort}(\mu', \tilde{a}) : e$

$E, (\sigma, \mu \text{find}[\text{unique?}] (\bigoplus_{j=1}^m u_{j1}[\tilde{i}] = i_{j1} \le n_{j1}, \dots, u_{jm_j}[\tilde{i}] = i_{jm_j} \le n_{jm_j} \text{ suchthat} \\ D_j \wedge M_j \text{ then } P_j) \text{ else } P) :: St, Q, Or, T, \mu \mathcal{E}v$

$$ \xrightarrow{p_1 \dots p_{l_0} D_{\text{find}}(S)(k_0)} \xrightarrow{t_1 \dots t_{l_0} F E(k_0)} E_{k_0}, (\sigma_{k_0}, \text{abort}) :: St, Q, Or, T, (\mu \mathcal{E}v, (\mu', \tilde{a})) : e $$

First four lines as in (FindT1) $S = \{v_k | r_k = \text{true}\} \quad |S| = 1 \text{ or } [\text{unique?}] \text{ is empty}$

$$ v_0 = (j', a'_1, \dots, a'_{m_{j'}}) \in S \qquad E' = E[u_{j'}[\sigma(\tilde{i})] \mapsto a'_1, \dots, u_{j'm_{j'}}[\sigma(\tilde{i})] \mapsto a'_{m_{j'}}] $$

$E, (\sigma, \mu \text{find}[\text{unique?}] (\bigoplus_{j=1}^m u_{j1}[\tilde{i}] = i_{j1} \le n_{j1}, \dots, u_{jm_j}[\tilde{i}] = i_{jm_j} \le n_{jm_j} \text{ suchthat} \\ D_j \wedge M_j \text{ then } P_j) \text{ else } P) :: St, Q, Or, T, \mu \mathcal{E}v$

$$ \xrightarrow{p_1 \dots p_l D_{\text{find}}(S)(v_0)} \xrightarrow{t_1 \dots t_l F_1(v_0)} E', (\sigma, P_j') :: St, Q, Or, T, \mu \mathcal{E}v \quad (\text{Find1}) $$

First four lines as in (FindT1) $S = \{v_k | r_k = \text{true}\} = \emptyset$

$E, (\sigma, \mu \text{find}[\text{unique?}] (\bigoplus_{j=1}^m u_{j1}[\tilde{i}] = i_{j1} \le n_{j1}, \dots, u_{jm_j}[\tilde{i}] = i_{jm_j} \le n_{jm_j} \text{ suchthat} \\ D_j \wedge M_j \text{ then } P_j) \text{ else } P) :: St, Q, Or, T, \mu \mathcal{E}v \xrightarrow{p_1 \dots p_l} t_1 \dots t_l F_2 E, (\sigma, P) :: St, Q, Or, T, \mu \mathcal{E}v$

(Find2)

First four lines as in (FindT1) $S = \{v_k | r_k = \text{true}\} \quad |S| > 1$

$E, (\sigma, \mu \text{find}[\text{unique}_e] (\bigoplus_{j=1}^m u_{j1}[\tilde{i}] = i_{j1} \le n_{j1}, \dots, u_{jm_j}[\tilde{i}] = i_{jm_j} \le n_{jm_j} \text{ suchthat } D_j \wedge \\ M_j \text{ then } P_j) \text{ else } P) :: St, Q, Or, T, \mu \mathcal{E}v$

$$ \xrightarrow{p_1 \dots p_l} \xrightarrow{t_1 \dots t_l F_3} E, (\sigma, \text{abort}) :: St, Q, Or, T, (\mu \mathcal{E}v, (\mu, \text{Im}(\sigma))) : e \quad (\text{Find3}) $$

$$ E, (\sigma, \mu \text{insert } \text{Tbl}(a_1, \dots, a_l); P) :: St, Q, Or, T, \mu \mathcal{E}v \qquad (\text{Insert}) \\ \xrightarrow{1} E, (\sigma, P) :: St, Q, Or, (T, \text{Tbl}(a_1, \dots, a_l)), \mu \mathcal{E}v $$

Same assumption as in (GetTE) $r_{k_0} = \text{event_abort}(\mu', \tilde{a}) : e$

$E, (\sigma, \mu \text{get}[\text{unique?}] \text{ Tbl}(x_1[\tilde{i}] : T_1, \dots, x_l[\tilde{i}] : T_l) \text{ suchthat } M \text{ in } P \text{ else } P') :: St, Q, Or, T, \mu \mathcal{E}v$

$$ \xrightarrow{p_1 \dots p_m D_{\text{get}}(S)(k_0)} \xrightarrow{t_1 \dots t_m G E(k_0)} E_{k_0}, (\sigma_{k_0}, \text{abort}) :: St, Q, Or, T, (\mu \mathcal{E}v, (\mu', \tilde{a})) : e \quad (\text{GetE}) $$

First four lines as in (GetT1) $|S| = 1 \text{ or } [\text{unique?}] \text{ is empty}$

$$ k_0 \in S \qquad \text{Tbl}(a_1, \dots, a_l) = v_{k_0} \qquad E' = E[x_1[\sigma(\tilde{i})] \mapsto a_1, \dots, x_l[\sigma(\tilde{i})] \mapsto a_l] $$

$E, (\sigma, \mu \text{get}[\text{unique?}] \text{ Tbl}(x_1[\tilde{i}] : T_1, \dots, x_l[\tilde{i}] : T_l) \text{ suchthat } M \text{ in } P \text{ else } P') :: St, Q, Or, T, \mu \mathcal{E}v$

$$ \xrightarrow{p_1 \dots p_m D_{\text{get}}(S)(k_0)} \xrightarrow{t_1 \dots t_m G_1(k_0)} E', (\sigma, P) :: St, Q, Or, T, \mu \mathcal{E}v \quad (\text{Get1}) $$

First four lines as in (GetT1) $S = \emptyset$

$E, (\sigma, \mu \text{get}[\text{unique?}] \text{ Tbl}(x_1[\tilde{i}] : T_1, \dots, x_l[\tilde{i}] : T_l) \text{ suchthat } M \text{ in } P \text{ else } P') :: St, Q, Or, T, \mu \mathcal{E}v$

$$ \xrightarrow{p_1 \dots p_m} \xrightarrow{t_1 \dots t_m G_2} E, (\sigma, P') :: St, Q, Or, T, \mu \mathcal{E}v \quad (\text{Get2}) $$

First four lines as in (GetT1) $|S| > 1$

$E, (\sigma, \mu \text{get}[\text{unique}_e] \text{ Tbl}(x_1[\tilde{i}] : T_1, \dots, x_l[\tilde{i}] : T_l) \text{ suchthat } M \text{ in } P \text{ else } P') :: St, Q, Or, T, \mu \mathcal{E}v$

$$ \xrightarrow{p_1 \dots p_m} \xrightarrow{t_1 \dots t_m G_3} E, (\sigma, \text{abort}) :: St, Q, Or, T, (\mu \mathcal{E}v, (\mu, \text{Im}(\sigma))) : e \quad (\text{Get3}) $$

<caption>Figure 9: Semantics (4): oracle bodies, first part</caption>
$$ \begin{array}{l} a \in T \qquad E' = E[x[\sigma(\tilde{i})] \mapsto a] \\ E, (\sigma, \mu x[\tilde{i}] \stackrel{R}{\leftarrow} T; P) :: St, Q, Or, T, \mu Ev \xrightarrow{D_T(a)} E', (\sigma, P) :: St, Q, Or, T, \mu Ev \end{array} \qquad \text{(New)} $$

$$ \begin{array}{l} a \in T \qquad E' = E[x[\sigma(\tilde{i})] \mapsto a] \\ E, (\sigma, \mu \text{let } x[\tilde{i}] : T = a \text{ in } P) :: St, Q, Or, T, \mu Ev \xrightarrow{1} E', (\sigma, P) :: St, Q, Or, T, \mu Ev \end{array} \qquad \text{(Let)} $$

$$ E, (\sigma, \mu \text{if true then } P \text{ else } P') :: St, Q, Or, T, \mu Ev \xrightarrow{1} E, (\sigma, P) :: St, Q, Or, T, \mu Ev \qquad \text{(If1)} $$

$$ a \neq true \qquad \frac{}{} \\ E, (\sigma, \mu \text{if } a \text{ then } P \text{ else } P') :: St, Q, Or, T, \mu Ev \xrightarrow{1} E, (\sigma, P') :: St, Q, Or, T, \mu Ev \qquad \text{(If2)} $$

$$ \begin{array}{l} E, (\sigma, \mu \text{event } e(a_1, \dots, a_l); P) :: St, Q, Or, T, \mu Ev \xrightarrow{1} \\ E, (\sigma, P) :: St, Q, Or, T, (\mu Ev, (\mu, \text{Im}(\sigma)) : e(a_1, \dots, a_l)) \end{array} \qquad \text{(Event)} $$

$$ E, (\sigma, \mu \text{event\_abort } e) :: St, Q, Or, T, \mu Ev \xrightarrow{1} E, (\sigma, \text{abort}) :: St, Q, Or, T, (\mu Ev, (\mu, \text{Im}(\sigma)) : e) \qquad \text{(EventAbort)} $$

$$ \begin{array}{l} E, \sigma, N, T, \mu Ev \xrightarrow{p} t E', \sigma', N', T', \mu Ev' \\ E, (\sigma, C[N]) :: St, Q, Or, T, \mu Ev \xrightarrow{p} t E', (\sigma', C[N']) :: St, Q, Or, T', \mu Ev' \end{array} \qquad \text{(Ctx)} $$

$$ \begin{array}{l} E, (\sigma, C[\text{event\_abort } (\mu, \tilde{a}) : e]) :: St, Q, Or, T, \mu Ev \xrightarrow{1} \\ E, (\sigma, \text{abort}) :: St, Q, Or, T, (\mu Ev, (\mu, \tilde{a}) : e) \end{array} \qquad \text{(CtxEvent)} $$

$$ P_0 = \text{let } x[\tilde{i}] : T = O[a_1, \dots, a_l, ?u_{l+1}[\tilde{i}] \le n_{l+1}, \dots, ?u_k[\tilde{i}] \le n_k](b) \text{ in } P_1 \text{ else } P_2 $$

$$ S = \{(\sigma', Q) \in Q | Q = \mu'' O[a_1, \dots, a_l, c_{l+1}, \dots, c_k](x'[\tilde{i}] : T') := P' \text{ and } b \in T' \text{ for some } \mu'', \sigma', x', T', P', c_{l+1} \in [1, n_{l+1}], \dots, c_k \in [1, n_k]\} $$

$$ (\sigma', Q_0) \in S \qquad Q_0 = \mu' O[a_1, \dots, a_k](x'[\tilde{i}] : T') := P' $$

$$ P'_0 = \text{let } x[\tilde{i}] : T = O[a_1, \dots, a_k](b) \text{ in } P_1 \text{ else } P_2 \qquad \text{(OracleCall)} $$

$$ \begin{array}{l} E, (\sigma, \mu P_0) :: St, Q, Or, T, \mu Ev \xrightarrow{S(\sigma', Q_0) \times D_{\text{call}}(S)(\sigma', Q_0)} O(\sigma', Q_0) \\ E[x'[\sigma'(\tilde{i})] \mapsto b, u_{l+1}[\sigma(\tilde{i})] \mapsto c_{l+1}, \dots, u_k[\sigma(\tilde{i})] \mapsto c_k], \\ (\sigma', P') :: (\sigma, \mu P'_0) :: St, Q \uplus \{(\sigma', Q_0)\}, Or, T, \mu Ev \end{array} $$

$$ \begin{array}{l} d \in T \qquad Q', Or' = \text{reduce}(\{(\sigma, Q)\}, Or) \\ P_0 = \text{let } x[\tilde{i}] : T = O[a_1, \dots, a_k](b) \text{ in } P_1 \text{ else } P_2 \\ \frac{}{} \\ E, (\sigma, \mu' \text{ return } (d); Q) :: (\sigma', \mu P_0) :: St, Q, Or, T, \mu Ev \xrightarrow{1} \\ E[x[\sigma'(\tilde{i})] \mapsto d], (\sigma', P_1) :: St, Q \uplus Q', Or', T, \mu Ev \end{array} \qquad \text{(Return)} $$

$$ \begin{array}{l} P_0 = \text{let } x[\tilde{i}] : T = O[a_1, \dots, a_k](b) \text{ in } P_1 \text{ else } P_2 \\ \frac{}{} \\ E, (\sigma, \mu' \text{ yield}) :: (\sigma', \mu P_0) :: St, Q, Or, T, \mu Ev \xrightarrow{1} E, (\sigma', P_2) :: St, Q, Or, T, \mu Ev \end{array} \qquad \text{(Yield)} $$

<caption>Figure 10: Semantics (5): oracle bodies, second part</caption>
$$
\begin{align*}
& Q', \mathcal{O}r' = \text{reduce}(\{(\sigma, Q)\}, \mathcal{O}r) \\
& S = \{(\sigma', Q) \in \mathcal{Q} \uplus Q' \mid \\
& \quad Q = \mu'' O[a_1, \dots, a_k](x'[\tilde{i}] : T') := P' \text{ and } b \in T' \\
& \quad \text{for some } \mu'', \sigma', x', \tilde{i}, T', P') \\
& \quad (\sigma', Q_0) \in S \quad Q_0 = \mu' O[a_1, \dots, a_k](x'[\tilde{i}] : T) := P' \\
& \quad \mathcal{A}(d) = D_{\mathcal{A}}^d \quad A_0, m_0 \stackrel{R}{\rightleftarrows} D_{\mathcal{A}}^d \quad m_0 = (O, a_1, \dots, a_k, b) \\
& \quad \mathcal{O}r' = (\mathcal{O}r'_{\text{pub}}, \mathcal{O}r'_{\text{priv}}) \quad O \notin \mathcal{O}r'_{\text{priv}} \\
& \mathcal{E}, (\sigma, \mu \text{ return } (d); Q) :: \mathcal{A}, \mathcal{Q}, \mathcal{O}r, \mathcal{T}, \mu \mathcal{E}v \xrightarrow{S(\sigma', Q_0) \times D_{\text{call}}(S)(\sigma', Q_0) \times D_{\mathcal{A}}^d(A_0, m_0)} \mathcal{O}(\sigma', Q_0, A_0, a_1, \dots, a_k, b) \\
& \mathcal{E}[x[\sigma'(\tilde{i})] \mapsto b], (\sigma', P') :: \mathcal{A}, \mathcal{Q} \uplus Q' \uplus \{(\sigma', Q_0)\}, \mathcal{O}r', \mathcal{T}, \mu \mathcal{E}v \tag{AttIO}
\end{align*}
$$

$$
\begin{align*}
& S = \{(\sigma', Q) \in \mathcal{Q} \mid Q = \mu'' O[a_1, \dots, a_k](x'[\tilde{i}] : T') := P' \text{ and } b \in T' \text{ for some } \mu'', \sigma', x', \tilde{i}, T', P' \} \\
& \qquad (\sigma', Q_0) \in S \quad Q_0 = \mu' O[a_1, \dots, a_k](x'[\tilde{i}] : T) := P' \\
& \qquad \mathcal{A}(\emptyset) = D_{\mathcal{A}}^{\emptyset} \quad A_0, m_0 \stackrel{R}{\rightleftarrows} D_{\mathcal{A}}^{\emptyset} \quad m_0 = (O, a_1, \dots, a_k, b) \\
& \qquad \mathcal{O}r = (\mathcal{O}r_{\text{pub}}, \mathcal{O}r_{\text{priv}}) \quad O \notin \mathcal{O}r_{\text{priv}} \\
& \mathcal{E}, (\sigma, \mu \text{ yield}) :: \mathcal{A}, \mathcal{Q}, \mathcal{O}r, \mathcal{T}, \mu \mathcal{E}v \xrightarrow{S(\sigma', Q_0) \times D_{\text{call}}(S)(\sigma', Q_0) \times D_{\mathcal{A}}^{\emptyset}(A_0, m_0)} \mathcal{O}(\sigma', Q_0, A_0, a_1, \dots, a_k, b) \\
& \mathcal{E}[x[\sigma'(\tilde{i})] \mapsto b], (\sigma', P') :: \mathcal{A}, \mathcal{Q} \uplus \{(\sigma', Q_0)\}, \mathcal{O}r, \mathcal{T}, \mu \mathcal{E}v \tag{AttYield}
\end{align*}
$$

<caption>Figure 11: Semantics (6): oracle bodies, third part, attackers interactions</caption>

We later show in Section 2.4.4 that there is in fact always at most one such possible oracle, and
that the probability only depends on attacker choices. Rule (AttYield) handles the case of a
yield returned to the attacker, where we then call the attacker with an empty input. This call is
disjoint from any other call to the attacker that could be performed through rule (AttIO): it is
assumed that the efficient bijection from types to concrete bitstrings does not return the empty
string.

After finishing execution of an oracle definition, the system produces as a result the sequence
of executed events $\mu\mathcal{E}v$. Looking forward, recall that an adversary will always be made of an
attacker $\mathcal{A}$ and an adversary context, this context thus allowing the adversary to raise arbitrary
values in the sequence of events.

These events can be used to distinguish games, so we introduce an additional algorithm,
a distinguisher $D$ that takes as input a sequence of events $\mathcal{E}v$ (without program points and
replication indices) and returns true or false.

An example of distinguisher is $D_e$ defined by $D_e(\mathcal{E}v) = \text{true if and only if } e \in \mathcal{E}v$: this distinguisher detects the execution of event $e$. We will denote the distinguisher $D_e$ simply by $e$. More generally, distinguishers can detect various properties of the sequence of events $\mathcal{E}v$ executed by the game and of its result $a$. We denote by $D \lor D'$, $D \land D'$, and $\neg D$ the distinguishers such that $(D \lor D')(\mathcal{E}v) = D(\mathcal{E}v) \lor D'(\mathcal{E}v)$, $(D \land D')(\mathcal{E}v) = D(\mathcal{E}v) \land D'(\mathcal{E}v)$, and $(\neg D)(\mathcal{E}v) = \neg D(\mathcal{E}v)$. We denote by $\text{Pr}[Q : D]$ the probability that $Q$ executes a sequence of events $\mathcal{E}v$ such that $D(\mathcal{E}v) = \text{true}$. This is formally defined as follows.

**Definition 4** The initial configuration for running oracle definition $Q$ against attacker $\mathcal{A}$ is $\text{initConfig}(Q, \mathcal{A}) = \emptyset$, $(\sigma_0, \text{return } (\text{start})) :: \mathcal{A}, \mathcal{Q}, \mathcal{O}r, \emptyset, \emptyset$ where $\mathcal{Q}, \mathcal{O}r = \text{reduce}(\{(\sigma_0, Q)\}, (\text{fo}(Q), \emptyset))$ and $\sigma_0$ is the empty mapping sequence. A trace of $Q$ for attacker $\mathcal{A}$ is a trace that starts from $\text{initConfig}(Q, \mathcal{A})$: $\text{Tr} = \text{initConfig}(Q, \mathcal{A}) \xrightarrow{p_1} t_1 \dots \xrightarrow{p_{m-1}} t_{m-1} \text{ Conf}_m$. Let $\mathcal{T}r^{A,Q}$ be the set of all traces of $Q$ for an attacker $\mathcal{A} \in \mathcal{BB}$.
C ::= $^{µ}$let $x[\tilde{i}] : T = []$ in P
$^{µ}$if [] then P else P'
$^{µ}$return ([]); Q
$^{µ}$let $x[\tilde{i}] : T = O[a_1, \dots, a_{k-1}, [], M_{k+1}, \dots, M_l, ?u_1[\tilde{i}] \le n_1, \dots, ?u_m[\tilde{i}] \le n_m](N)$ in P
else P'
$^{µ}$let $x[\tilde{i}] : T = O[a_1, \dots, a_l, ?u_1[\tilde{i}] \le n_1, \dots, ?u_m[\tilde{i}] \le n_m]([])$ in P else P'
$^{µ}$insert Tbl(a_1, \dots, a_{k-1}, [], M_{k+1}, \dots, M_l); P
$^{µ}$event $e(a_1, \dots, a_{k-1}, [], M_{k+1}, \dots, M_l); P$

<caption>Figure 12: Oracle contexts</caption>

Let $\mathcal{T}r_{\text{full}}^{A,Q}$ be the set of full traces of $Q$, that is, the set of traces of $\mathcal{T}r^{A,Q}$ whose last configuration $Conf_m$ cannot be reduced.

A trace $Tr'$ is an extension of $Tr$ when $Tr'$ is obtained by continuing execution from the last configuration of $Tr$. Equivalently, $Tr$ is a prefix of $Tr'$.

Let $\varphi$ be a property of traces, that is, a function from traces to $\{\text{true, false}\}$. We say that $Tr$ satisfies $\varphi$, and we write $Tr \vdash \varphi$, when $\varphi(Tr) = \text{true}$.

A property $\varphi$ is preserved by extension when for all traces $Tr$ such that $Tr \vdash \varphi$, for all extensions $Tr'$ of $Tr$, $Tr' \vdash \varphi$.

Given a trace $Tr = \text{initConfig}(Q, \mathcal{A}) \xrightarrow{p_1} t_1 \dots \xrightarrow{p_{m-1}} t_{m-1} \text{ Conf}_m$, recall that $\text{Pr}[Tr] = p_1 \times \dots \times p_{m-1}$. We define

$$
\begin{align*}
\Pr^{\mathcal{A}}[Q : \varphi] &= \sum_{Tr \in \mathcal{T}r_{\text{full}}^{A,Q}, Tr \vdash \varphi} \Pr[Tr], \\
\Pr^{\mathcal{A}}[Q \preceq \varphi] &= \sum_{Tr \in \mathcal{T}r_{\text{full}}^{A,Q}, \exists Tr' \text{ prefix of } Tr, Tr' \vdash \varphi} \Pr[Tr] \\
&= \sum_{Tr \in \mathcal{T}r^{A,Q}, Tr \vdash \varphi, \text{for any strict prefix } Tr' \text{ of } Tr, Tr' \not\vdash \varphi} \Pr[Tr].
\end{align*}
$$

Given a distinguisher $D$, we can consider it as a property of traces by defining $Tr \vdash D$ if and only if $D(\text{removepp}(\mu\mathcal{E}v_m)) = \text{true}$ where the last configuration of $Tr$ is $Conf_m = E_m, St_m, Q_m, Or_m, T_m, \mu\mathcal{E}v_m$. The function removepp guarantees that the pair (program point, replication indices) is not used in the evaluation of the distinguisher. Actually, this pair could be removed from the semantics. It is useful for the proof of injective correspondences (Section 4.2.4).

**Lemma 1** 1. $\Pr^A[Q : \varphi] \le \Pr^A[Q \preceq \varphi]$.

2. If $\varphi$ is preserved by extension, then $\Pr^A[Q : \varphi] = \Pr^A[Q \preceq \varphi]$.

**Proof** The first property holds because, when $Tr \vdash \varphi$, there exists a prefix $Tr'$ of $Tr$ (take $Tr' = Tr$) such that $Tr' \vdash \varphi$.

The second property holds because, if $\varphi$ is preserved by extension and there exists a prefix $Tr'$ of $Tr$ such that $Tr' \vdash \varphi$, then $Tr \vdash \varphi$. $\square$
For simple terms $M$, the evaluation can be defined without tables and events. We define $E, \rho, M \Downarrow a$ if and only if $E, \rho, M, \emptyset, \emptyset \xrightarrow{1}^* E, \rho, a, \emptyset, \emptyset$, where the environment $E$ gives the values of process variables (in particular arrays), and the environment $\rho$ gives the values of replication indices and other variables (e.g., those used in correspondences, see Section 2.8.3). The evaluation relation $E, \rho, M \Downarrow a$ can also be defined by induction as follows:

$$ \frac{E, \rho, i \Downarrow \rho(i) \quad \forall j \le m, E, \rho, M_j \Downarrow a_j}{E, \rho, x[M_1, \dots, M_m] \Downarrow E(x[a_1, \dots, a_m])} $$ $$ \frac{\forall j \le m, E, \rho, M_j \Downarrow a_j}{E, \rho, f(M_1, \dots, M_m) \Downarrow f(a_1, \dots, a_m)} $$

For terms that do not contain process variables, the environment $E$ can be omitted, and we write $\rho, M \Downarrow a$. It can also be defined by induction as follows:

$$ \frac{\rho, i \Downarrow \rho(i) \quad \forall j \le m, \rho, M_j \Downarrow a_j}{\rho, f(M_1, \dots, M_m) \Downarrow f(a_1, \dots, a_m)} $$

## 2.4.2 Properties

Given an oracle definition $Q_0$, we write $I_\mu$ for the current replication indices at $\mu$ in $Q_0$. For $^\mu\text{return} (start)$ in the initial configuration, we let $I_\mu = \emptyset$ be the empty sequence.

**Lemma 2** Let $\mathcal{T}$ be a trace of $Q_0$ for any $A \in \mathcal{B}\mathcal{B}$. In the derivation of $\mathcal{T}$, for all configurations $E, \sigma, ^\mu M, \mathcal{T}, \mu\mathcal{E}v$, $\text{Dom}(\sigma) = I_\mu$; for all configurations $E, \text{St}, \mathcal{Q}, \text{Or}, \mathcal{T}, \mu\mathcal{E}v$, for all $(\sigma, ^\mu P) \in \text{St}$, $\text{Dom}(\sigma) = I_\mu$; and for all configurations $\mathcal{Q}, \text{Or}$ or $E, \text{St}, \mathcal{Q}, \text{Or}, \mathcal{T}, \mu\mathcal{E}v$, for all $(\sigma, ^\mu Q) \in \mathcal{Q}$, $\text{Dom}(\sigma) = I_\mu$.

**Proof sketch** We say that

* a configuration $E, \sigma, ^\mu M, \mathcal{T}, \mu\mathcal{E}v$ is ok when $\text{Dom}(\sigma) = I_\mu$;

* a configuration $\mathcal{Q}, \text{Or}$ is ok when for all $(\sigma, ^\mu Q) \in \mathcal{Q}$, $\text{Dom}(\sigma) = I_\mu$;

* a configuration $E, \text{St}, \mathcal{Q}, \text{Or}, \mathcal{T}, \mu\mathcal{E}v$ is ok when for all $(\sigma, ^\mu P) \in \text{St}$, $\text{Dom}(\sigma) = I_\mu$ and for all $(\sigma, ^\mu Q) \in \mathcal{Q}$, $\text{Dom}(\sigma) = I_\mu$.

We show by induction on the derivations that

1. if $E_1, \sigma_1, M_1, \mathcal{T}_1, \mu\mathcal{E}v_1$ is ok, then all configurations $E, \sigma, M, \mathcal{T}, \mu\mathcal{E}v$ in the derivation of $E_1, \sigma_1, M_1, \mathcal{T}_1, \mu\mathcal{E}v_1 \xrightarrow{p} E_2, \sigma_2, M_2, \mathcal{T}_2, \mu\mathcal{E}v_2$ are ok;

2. if $\mathcal{Q}_1, \text{Or}_1$ is ok and $\mathcal{Q}_1, \text{Or}_1 \rightsquigarrow \mathcal{Q}_2, \text{Or}_2$, then $\mathcal{Q}_2, \text{Or}_2$ is ok;

3. if $\mathcal{Q}_1, \text{Or}_1$ is ok, then reduce($\mathcal{Q}_1, \text{Or}_1$) is ok and all configurations $\mathcal{Q}, \text{Or}$ and in the derivation of $\mathcal{Q}_1, \text{Or}_1 \rightsquigarrow^* \mathcal{Q}_1, \text{Or}_1$ are ok;

4. if $E_1, \text{St}_1, \mathcal{Q}_1, \text{Or}_1, \mathcal{T}_1, \mu\mathcal{E}v_1$ is ok, then all configurations $E, \sigma, M, \mathcal{T}, \mu\mathcal{E}v$ or $\mathcal{Q}, \text{Or}$ or $E, \text{St}, \mathcal{Q}, \text{Or}, \mathcal{T}, \mu\mathcal{E}v$ in the derivation of $E_1, \text{St}_1, \mathcal{Q}_1, \text{Or}_1, \mathcal{T}_1, \mu\mathcal{E}v_1 \xrightarrow{p} E_2, \text{St}_2, \mathcal{Q}_2, \text{Or}_2, \mathcal{T}_2, \mu\mathcal{E}v_2$ are ok.
Indeed, the changes in $\sigma$ match the definition of replication indices.

For Property 1, in rules for find, the indices of the find condition are added to the domain of $\sigma$ when evaluating the condition and in all other cases, $\sigma$ is unchanged.

In the proof of Property 2, in (Repl), the replication index $i$ is added to $\sigma$ and in all other cases, $\sigma$ is unchanged.

Property 3 follows immediately from Property 2 by induction.

For Property 4, in rules for find, the indices of the find condition are added to the domain of $\sigma$ when evaluating the condition, as in Property 1; in (Return), we use Property 3. In all other cases, $\sigma$ is unchanged and remains associated with the same program point or a program point with the same replication indices. We use Property 1 when evaluating terms, in conditions of find and get and in (Ctx).

Moreover, in the computation of initConfig($Q_0$, $\mathcal{A}$), the configuration $\{(\sigma_0, Q_0)\}$, $(\text{fo}(Q), \emptyset)$ is ok (the current replication indices at the root of $Q_0$ are empty), so by Property 3, initConfig($Q_0$, $\mathcal{A}$) is ok. $\square$

**Lemma 3** If $E, \sigma, N, T, \mu\mathcal{E}v \xrightarrow{p} t E', \sigma', N', T', \mu\mathcal{E}v'$, then $E'$ is an extension of $E$, $T$ is a prefix of $T'$, $\mu\mathcal{E}v$ is a prefix of $\mu\mathcal{E}v'$, $\sigma'$ is an extension of $\sigma$, and if the term $N'$ is not of the form $C_1[\dots C_k[\text{event_abort} (\mu, \tilde{a}) : e]\dots]$ for some $k \in \mathbb{N}$ and $C_1, \dots, C_k$ contexts defined in Figure 7, then $\sigma' = \sigma$. For all configurations $E'', \sigma'', N'', T'', \mu\mathcal{E}v''$ in the derivation of $E, \sigma, N, T, \mu\mathcal{E}v \xrightarrow{p} t E', \sigma', N', T', \mu\mathcal{E}v'$, we have that $E''$ is an extension of $E$ and, if $E'', \sigma'', N'', T'', \mu\mathcal{E}v''$ is not in the derivation of an hypothesis of a rule for find or get, then $E'$ is an extension of $E''$; $\sigma''$ is an extension of $\sigma$; $T$ is a prefix of $T''$, which is a prefix of $T'$; and $\mu\mathcal{E}v$ is a prefix of $\mu\mathcal{E}v''$, which is a prefix of $\mu\mathcal{E}v'$.

If $Q, (Or_{\text{pub}}, Or_{\text{priv}}) \rightsquigarrow Q', (Or'_{\text{pub}}, Or'_{\text{priv}})$, then $Or'_{\text{pub}} = Or_{\text{pub}}$ and $Or_{\text{priv}} \subseteq Or'_{\text{priv}}$.

If $E, (\sigma, P) :: St, Q, (Or_{\text{pub}}, Or_{\text{priv}}), T, \mu\mathcal{E}v \xrightarrow{p} t E', (\sigma', P') :: St', Q', (Or'_{\text{pub}}, Or'_{\text{priv}}), T', \mu\mathcal{E}v'$, then $E'$ is an extension of $E$, $T$ is a prefix of $T'$, $\mu\mathcal{E}v$ is a prefix of $\mu\mathcal{E}v'$, $Or_{\text{pub}} = Or'_{\text{pub}}$ and $Or_{\text{priv}} \subseteq Or'_{\text{priv}}$.

* If $E, (\sigma, P) :: St, Q, (Or_{\text{pub}}, Or_{\text{priv}}), T, \mu\mathcal{E}v \xrightarrow{p} t E', (\sigma', P') :: St', Q', (Or'_{\text{pub}}, Or'_{\text{priv}}), T', \mu\mathcal{E}v'$ is derived by (Return) or (AttIO), then $T' = T, \mu\mathcal{E}v' = \mu\mathcal{E}v$, and for all configurations $Q'', Or''$ in that derivation, $Or_{\text{priv}} \subseteq Or'_{\text{priv}} \subseteq Or'_{\text{priv}}$ and $Or_{\text{pub}} = Or''_{\text{pub}} = Or'_{\text{pub}}$.

* If $E, (\sigma, P) :: St, Q, (Or_{\text{pub}}, Or_{\text{priv}}), T, \mu\mathcal{E}v \xrightarrow{p} t E', (\sigma', P') :: St', Q', (Or'_{\text{pub}}, Or'_{\text{priv}}), T', \mu\mathcal{E}v'$ is derived by (Yield), (OracleCall), or (AttYield), then $T' = T, \mu\mathcal{E}v' = \mu\mathcal{E}v$, $Or_{\text{priv}} = Or'_{\text{priv}}$, and $Or_{\text{pub}} = Or'_{\text{pub}}$.

* In all other cases, $Or'_{\text{pub}} = Or_{\text{pub}}, Or'_{\text{priv}} = Or_{\text{priv}}, St = St', \sigma'$ is an extension of $\sigma$, and if the oracle body $P'$ is not abort or of the form $C_0[C_1[\dots C_k[\text{event_abort} (\mu, \tilde{a}) : e]\dots]]$ for some $C_0$ context defined in Figure 12, $k \in \mathbb{N}$, and $C_1, \dots, C_k$ contexts defined in Figure 7, then $\sigma' = \sigma$. For all configurations $E'', \sigma'', N'', T'', \mu\mathcal{E}v''$ in the derivation of $E, (\sigma, P) :: St, Q, (Or_{\text{pub}}, Or_{\text{priv}}), T, \mu\mathcal{E}v \xrightarrow{p} t E', (\sigma', P') :: St', Q', (Or'_{\text{pub}}, Or'_{\text{priv}}), T', \mu\mathcal{E}v'$, we have that $E''$ is an extension of $E$ and, if $E'', \sigma'', N'', T'', \mu\mathcal{E}v''$ is not in the derivation of an hypothesis of a rule for find or get, then $E'$ is an extension of $E''$; $\sigma''$ is an extension of $\sigma$; $T$ is a prefix of $T''$, which is a prefix of $T'$; and $\mu\mathcal{E}v$ is a prefix of $\mu\mathcal{E}v''$, which is a prefix of $\mu\mathcal{E}v'$.

**Proof sketch** By induction on the derivation of $E, \sigma, N, T, \mu\mathcal{E}v \xrightarrow{p} t E', \sigma', N', T', \mu\mathcal{E}v'$ and by cases on the reductions $Q, Or \rightsquigarrow Q', Or'$ and $E, St, Q, Or, T, \mu\mathcal{E}v \xrightarrow{p} t E', St', Q', Or', T', \mu\mathcal{E}v'$.

<figure><img src="image_5.png" /></figure>
We say that a term $N$ is in evaluation position in a configuration $E, \sigma, M, \mathcal{T}, \mu\mathcal{E}v$ when $M = C_1[\dots C_k[N]\dots]$ for some $k \in \mathbb{N}$ and $C_1, \dots, C_k$ contexts defined in Figure 7.

We say that a term $N$ is in evaluation position in a configuration $E, (\sigma, P) :: St, Q, Or, \mathcal{T}, \mu\mathcal{E}v$ when $P = C_0[C_1[\dots C_k[N]\dots]]$ for some $C_0$ context defined in Figure 12, $k \in \mathbb{N}$, and $C_1, \dots, C_k$ contexts defined in Figure 7, or $(\sigma', \text{let } x[i]: T = O[a_1, \dots, a_k](b) \text{ in } P_1 \text{ else } P_2) \in St$ and $N$ is $a_1, \dots, a_k$, or $b$.

The oracle bodies $P$ such that $(\sigma, P) \in St$ for some $\sigma$ are in evaluation position in configuration $E, St, Q, Or, \mathcal{T}, \mu\mathcal{E}v$. The oracle definitions $Q$ such that $(\sigma, Q) \in Q$ for some $\sigma$ are in evaluation position in configurations $Q, Or$ and $E, St, Q, Or, \mathcal{T}, \mu\mathcal{E}v$.

**Lemma 4** Consider a trace $\text{Tr}$ of $Q_0$ for any $\mathcal{A} \in \mathcal{BB}$.

All subterms of $M$ that occur in non-evaluation position in a configuration $E, \sigma, M, \mathcal{T}, \mu\mathcal{E}v$ in the derivation of $\text{Tr}$ are subterms of $Q_0$.

All subterms and subprocesses of oracle definitions in $Q$ that occur in non-evaluation position in a configuration $Q, Or$ in the derivation of $\text{Tr}$ are subterms, resp. subprocesses, of $Q_0$ up to renaming of oracles. All subterms and subprocesses of $St$ and of $Q$ that occur in non-evaluation position in a configuration $E, St, Q, Or, \mathcal{T}, \mu\mathcal{E}v$ in the derivation of $\text{Tr}$ are subterms, resp. subprocesses, of $Q_0$ up to renaming of oracles (except for the process 0 that follows return (start) in `initConfig($Q_0, \mathcal{A}$)`).

**Proof** We say that

* a configuration $E, \sigma, M, \mathcal{T}, \mu\mathcal{E}v$ is ok when all subterms of $M$ that are not in evaluation position are subterms of $Q_0$;

* a configuration $Q, Or$ is ok when all subterms and subprocesses of $Q$ that are not in evaluation position are subterms, resp. subprocesses, of $Q_0$ up to renaming of oracles;

* a configuration $E, St, Q, Or, \mathcal{T}, \mu\mathcal{E}v$ is ok when all subterms and subprocesses of $St$ and of $Q$ that are not in evaluation position are subterms, resp. subprocesses, of $Q_0$ up to renaming of oracles.

We show by induction on the derivations that

1. if $E_1, \sigma_1, M_1, \mathcal{T}_1, \mu\mathcal{E}v_1$ is ok, then all configurations $E, \sigma, M, \mathcal{T}, \mu\mathcal{E}v$ in the derivation of $E_1, \sigma_1, M_1, \mathcal{T}_1, \mu\mathcal{E}v_1 \xrightarrow{p} t E_2, \sigma_2, M_2, \mathcal{T}_2, \mu\mathcal{E}v_2$ are ok;

2. if $Q_1, Or_1$ is ok and $Q_1, Or_1 \rightsquigarrow Q_2, Or_2$, then $Q_2, Or_2$ is ok;

3. if $Q_1, Or_1$ is ok, then reduce($Q_1, Or_1$) is ok and all configurations $Q, Or$ in the derivation of $Q_1, Or_1 \rightsquigarrow^* Q_1, Or_1$ are ok;

4. if $E_1, St_1, Q_1, Or_1, \mathcal{T}_1, \mu\mathcal{E}v_1$ is ok, then all configurations $E, \sigma, M, \mathcal{T}, \mu\mathcal{E}v$ or $Q, Or$ or $E, St, Q, Or, \mathcal{T}, \mu\mathcal{E}v$ in the derivation of $E_1, St_1, Q_1, Or_1, \mathcal{T}_1, \mu\mathcal{E}v_1 \xrightarrow{p} t E_2, St_2, Q_2, Or_2, \mathcal{T}_2, \mu\mathcal{E}v_2$ are ok.

**Property 1:** In (ReplIndex), (Var), (Fun), and (EventAbortT), all terms are in evaluation position, so all configurations are ok. In (NewT), (LetT), (IfT1), (IfT2), (InsertT), and (EventT), $N$ (resp. $N'$) is not in evaluation position, so by hypothesis it is a subterm of $Q_0$. Therefore, the target configuration is ok. In the rules for find, the recursive calls are on $D_j \wedge M_j$ which is not in evaluation position, so it is a subterm of $Q_0$. Therefore, the initial configurations of the recursive calls are ok, and we conclude for the configurations inside the recursive calls by induction hypothesis. The target configuration is ok because in (FindTE) and (FindT3), the resulting
term is in evaluation position (it has no subterm), and in (FindT1) and (FindT2), the resulting term is a term that is not evaluation position in the initial configuration, so it is a subterm of $Q_0$. In (DefinedNo) and (DefinedYes), the terms $M_1, \dots, M_l$ are not in evaluation position in the initial configuration, so they are subterms of $Q_0$. Hence the initial configurations of the recursive calls are ok, and we conclude for the configurations inside the recursive calls by induction hypothesis. The target configuration is ok because in (DefinedNo), false is in evaluation position (it has no subterm) and in (DefinedYes), the resulting term $M$ is a term that is not evaluation position in the initial configuration, so it is a subterm of $Q_0$. The case of get is similar to the one of find. In (CtxT), the initial configuration of the recursive call is ok because terms that are not in evaluation position in $N$ are also not in evaluation position in $C[N]$, so they are subterms of $Q_0$. We conclude for the configurations inside the recursive call by induction hypothesis. The target configuration is ok because terms that are not in evaluation position in $C[N']$ are either not in evaluation position inside $C$, in which case they are subterms of $Q_0$ because the initial configuration is ok, or they are not in evaluation position in $N'$, in which case they are also subterms of $Q_0$ because the target configuration of the recursive call is ok. In (CtxEventT), the target configuration is ok because the term is in evaluation position (it has no subterm).

**Property 2:** The desired property is preserved for unmodified oracle definitions in $Q$. This is enough to conclude for (Nil). For (Par) and (Repl), the resulting oracle definitions $Q_1, Q_2, Q$ are not in evaluation position in the initial configuration, so they are subprocesses of $Q_0$ up to renaming of oracles. For (NewOracle), $Q$ is not in evaluation position in the initial configuration, so it is a subprocess of $Q_0$ up to renaming of oracles, and so is $Q\{O'/O\}$. For (DefOracle), the target configuration is ok because the subterms or subprocesses not in evaluation position are subterms or subprocesses of $P$, which are not in evaluation position in the initial configuration, so that are subterms or subprocesses of $Q_0$ up to renaming of oracles.

Property 3 follows immediately from Property 2 by induction.

**Property 4:** In (Return), (AttYield) or (AttIO), $Q$ is not in evaluation position in the initial configuration, so it is a subprocess of $Q_0$ up to renaming of oracles. Therefore, the configuration $\{(\sigma, Q)\}, Or$ is ok. By Property 3, all configurations in the computation of $Q', Or'$ and $Q', Or'$ itself are ok. Moreover, in (Return), $P_1$ is not in evaluation position in the initial configuration, so it is a subprocess of $Q_0$ up to renaming of oracles. We can then conclude that the target configuration is ok. In (AttIO) or (AttYield), $P'$ is not in evaluation position in the initial configuration, so it is a subprocess of $Q_0$ up to renaming of oracles. We can then conclude that the target configuration is ok. Rule (OracleCall) is similar with $P', P_1, P_2$ also not in evaluation position in the initial configuration. In (Yield), $P_2$ is not in evaluation position in the initial configuration. All other cases can be treated similarly to terms in Property 1. Moreover, in the computation of initConfig($Q_0$, $A$), the configuration $\{(\sigma_0, Q_0)\}$, ($\text{fo}(Q), \emptyset$) is ok, so by Property 3, initConfig($Q_0$, $A$) is ok except for the process 0 that follows return (start) in initConfig($Q_0$, $A$). That process disappears in the first reduction, which is by (AttIO). $\square$

**Corollary 1** Consider a trace $\text{Tr}$ of $Q_0$ for any $A \in \mathcal{B}\mathcal{B}$.

In $\text{Tr}$, the target oracle body of rules (New), (Let), (If1), (If2), (Find1), (Find2), (Insert), (Get1), (Get2), (OracleCall), (Return), (Yield), (AttIO), (AttYield), (Event) is a subprocess of $Q_0$ up to renaming of oracles.

In $\text{Tr}$, the target term of rules (NewT), (LetT), (IfT1), (IfT2), (FindT1), (FindT2), (InsertT), (GetT1), (GetT2), (EventT), (DefinedYes) is a subterm $Q_0$.

**Proof** The target term or oracle body of these rules appears in non-evaluation position in the initial configuration of these rules, so by Lemma 4, it is a subterm of $Q_0$ or a subprocess of $Q_0$ up to renaming of oracles. $\square$
We say that a configuration Conf is at program point $\mu$ in a trace $Tr$ of $Q_0$ when Conf occurs in the derivation of $Tr$, and either $Conf = E, \sigma, \mu N, T, \mu Ev$ for some subterm $\mu N$ of $Q_0$ or $Conf = E, (\sigma, \mu P) :: St, Q, Or, T, \mu Ev$ for some subprocess $\mu P$ of $Q_0$ up to renaming of oracles.

**Lemma 5** Let $Tr$ be a trace of $Q_0$ for any $A \in \mathcal{B}\mathcal{B}$. Let Conf be a configuration at program point $\mu$ in $Tr$. If $\mu$ is not inside a condition of find or get, then Conf is not in the derivation of an hypothesis of a rule for find or get inside the derivation of $Tr$.

**Proof** The only rules that can conclude with a term find or get are (NewT), (LetT), (IfT1), (IfT2), (FindT1), (FindT2), (InsertT), (GetT1), (GetT2), (EventT), (DefinedYes) and, by Corollary 1, their target term is a subterm of $Q_0$. The situation is similar find and get processes. So the executed term or oracle in the initial configuration of rules for find and get is always a subterm or subprocess of $Q_0$ up to renaming of oracles. When a configuration Conf is in the derivation of an hypothesis of a rule for find or get, it therefore always deals with program points syntactically in conditions of find or get in $Q_0$. (The semantic rules do not create program points.) Since $\mu$ is not inside a condition of find or get, we conclude that Conf is not in the derivation of an hypothesis of a rule for find or get. $\square$

Given a trace $Tr$, we define a partial ordering relation $\leq_{Tr}$ (reflexive, transitive, antisymmetric) on the occurrences of configurations in the derivation of $Tr$: if $Conf_1 \stackrel{p}{\rightarrow} Conf_2$ occurs in the derivation of $Tr$, then $Conf_1 \leq_{Tr} Conf_2$ and for all Conf that occur in the derivation of the assumptions of $Conf_1 \stackrel{p}{\rightarrow} Conf_2$, $Conf_1 \leq_{Tr} Conf_2 \leq_{Tr} Conf_2$, and similarly for $\rightsquigarrow$ instead of $\stackrel{p}{\rightarrow}_t$. If $Tr$ is a trace of $Q_0$ for $A$, then for all Conf that occur in the derivation of $\{(\sigma_0, Q_0)\}, (\text{fo}(Q_0), \emptyset) \rightsquigarrow * Q, Or$, we have $Conf \leq_{Tr} \text{initConfig}(Q_0, A)$. When $Conf_1 \leq_{Tr} Conf_2$, we say that $Conf_1$ occurs before $Conf_2$ in $Tr$, or equivalently, that $Conf_2$ occurs after $Conf_1$ in $Tr$.

We say that a configuration $Conf = E, \sigma, \mu N, T, \mu Ev$, $Conf = E, St, Q, Or, T, \mu Ev$ with $(\sigma', \mu Q) \in Q$, or $(\sigma', \mu P) \in St$, or $Conf = Q, Or$ with $(\sigma', \mu Q) \in Q$ is inside program point $\mu$. A configuration may be inside several program points: $Conf = Q, Or$ is inside the program points of the oracle definitions in $Q$, $Conf = E, St, Q, Or, T, \mu Ev$ is inside the program points of the oracle bodies in $St$ as well as the oracle definitions in $Q$.

We say that the program point $\mu$ is immediately above the program points $\mu_j$ in a process $Q_0$ when $Q_0$ contains one of the following constructs:

$$^{\mu}x[\mu_1 M_1, \dots, \mu_m M_m]$$

$$^{\mu}f(\mu_1 M_1, \dots, \mu_m M_m)$$

$$^{\mu}x[\tilde{i}] \stackrel{R}{\leftarrow} T; \mu_1 N$$

$$^{\mu}\text{let } x[\tilde{i}] : T = \mu_1 M \text{ in } \mu_2 N$$

$$^{\mu}\text{if } \mu_1 M \text{ then } \mu_2 N \text{ else } \mu_3 N'$$

$$^{\mu}\text{find}[\text{unique?}] (\bigoplus_{j=1}^{m} u_{j1}[\tilde{i}] = i_{j1} \le n_{j1}, \dots, u_{jm_j}[\tilde{i}] = i_{jm_j} \le n_{jm_j} \text{ suchthat} \\ \text{defined}(\mu_{j,1} M_{j1}, \dots, \mu_{j,l_j} M_{jl_j}) \wedge \mu_{j,t_j+1} M'_j \text{ then } \mu_{j,t_j+2} N_j) \text{ else } \mu_0 N'$$

$$^{\mu}\text{insert } Tbl(\mu_1 M_1, \dots, \mu_l M_l); \mu_0 N$$

$$^{\mu}\text{get}[\text{unique?}] Tbl(x_1[\tilde{i}] : T_1, \dots, x_l[\tilde{i}] : T_l) \text{ suchthat } \mu_1 M \text{ in } \mu_2 N \text{ else } \mu_3 N'$$

$$^{\mu}\text{event } e(\mu_1 M_1, \dots, \mu_l M_l); \mu_0 N$$

$$^{\mu}(\mu_1 Q | \mu_2 Q')$$
$$^{\mu}\text{foreach } i \leq n \text{ do } ^{\mu_1}Q$$

$$^{\mu}\text{newOracle } O; ^{\mu_1}Q$$

$$^{\mu}O[\tilde{i}](x[\tilde{i}] : T) := ^{\mu_0}P$$

$$^{\mu}\text{return } (^{\mu_1}M); ^{\mu_2}Q$$

$$^{\mu}\text{let } x[\tilde{i}] : T = O[^{\mu_1}M_1, \dots, ^{\mu_l}M_l, ?u_1[\tilde{i}] \leq n_1, \dots, ?u_m[\tilde{i}] \leq n_m](^{\mu_0}M) \text{ in } ^{\mu'_1}P_1 \text{ else } ^{\mu'_2}P_2$$

$$^{\mu}x[\tilde{i}] \stackrel{R}{\leftarrow} T; ^{\mu_1}P$$

$$^{\mu}\text{let } x[\tilde{i}] = ^{\mu_1}M \text{ in } ^{\mu_2}P$$

$$^{\mu}\text{if } ^{\mu_1}M \text{ then } ^{\mu_2}P \text{ else } ^{\mu_3}P'$$

$$^{\mu}\text{find}[\text{unique?}] \left( \bigoplus_{j=1}^{m} u_{j1}[\tilde{i}] = i_{j1} \leq n_{j1}, \dots, u_{jm_j}[\tilde{i}] = i_{jm_j} \leq n_{jm_j} \text{ suchthat } \text{defined}(^{\mu_{j,1}}M_{j1}, \dots, ^{\mu_{j,l_j}}M_{jl_j}) \wedge ^{\mu_{j,l_j+1}}M_j \text{ then } ^{\mu_{j,l_j+2}}P_j \text{ else } ^{\mu_0}P \right)$$

$$^{\mu}\text{insert } \text{Tbl}(^{\mu_1}M_1, \dots, ^{\mu_l}M_l); ^{\mu_0}P$$

$$^{\mu}\text{get}[\text{unique?}] \text{Tbl}(x_1[\tilde{i}] : T_1, \dots, x_l[\tilde{i}] : T_l) \text{ suchthat } ^{\mu_1}M \text{ in } ^{\mu_2}P \text{ else } ^{\mu_3}P'$$

$$^{\mu}\text{event } e(^{\mu_1}M_1, \dots, ^{\mu_l}M_l); ^{\mu_0}P$$

The relation "$\mu$ is above $\mu'$" is the reflexive and transitive closure of "$\mu$ is immediately above $\mu'$".

**Lemma 6** Let $\mathbf{Tr}$ be a trace of $Q_0$ for any $\mathcal{A} \in \mathcal{BB}$. If $\mathbf{Conf}$ is a configuration in $\mathbf{Tr}$ inside program point $\mu$ and $\mu$ is a program point in $Q_0$, then either $\mathbf{Conf}$ is at the program point $\mu$ at the top of $Q_0$, or there exists a configuration $\mathbf{Conf}' \neq \mathbf{Conf}$ such that $\mathbf{Conf}' \preceq_{\mathbf{Tr}} \mathbf{Conf}$ and $\mathbf{Conf}'$ is inside program point $\mu$ or inside the program point $\mu'$ immediately above $\mu$ in $Q_0$.

As a consequence, if a configuration $\mathbf{Conf}$ inside program point $\mu$ in $Q_0$ is in $\mathbf{Tr}$, then there are configurations inside all program points above $\mu$ in $Q_0$ before $\mathbf{Conf}$ in $\mathbf{Tr}$.

**Proof** First property. Since $\mathbf{Conf}$ is a configuration in $\mathbf{Tr}$, we are in one of the following cases:

* $\mathbf{Conf} = \{(\sigma_0, Q_0)\}$, $(\text{fo}(Q_0), \emptyset)$, the very first configuration of $\mathbf{Tr}$. The configuration $\mathbf{Conf}$ is at the program point $\mu$ at the top of $Q_0$.

* $\mathbf{Conf} = \text{initConfig}(Q_0, \mathcal{A}) = \emptyset$, $(\sigma_0, \mu'' \text{return } (\text{start})) :: \mathcal{A}, \mathcal{Q}, \mathcal{Or}, \emptyset, \emptyset$. Since $\mu''$ is not in $Q_0$, $\mu$ is the program point of an oracle declaration in $\mathcal{Q}$. Then $\mathbf{Conf}' = \mathcal{Q}, \mathcal{Or}$ is also inside $\mu$ and $\mathbf{Conf}' \preceq_{\mathbf{Tr}} \mathbf{Conf}$, by definition of $\preceq_{\mathbf{Tr}}$.

* $\mathbf{Conf}$ is the initial configuration of an assumption of a semantic rule. In rules for find, the initial configuration of the assumption is not inside a program point (because it evaluates the defined condition, not a term). In rules for get, (CxtT), and (Ctx), the initial configuration of the conclusion is inside the program point $\mu'$ immediately above $\mu$. In rules (DefinedNo) and (DefinedYes), these rules are used to conclude assumptions of find, and the initial configuration of the find rule is inside the program point $\mu'$ immediately above $\mu$. In rules (Return) and (AttIO), $\mathbf{Conf} = \{(\sigma, Q)\}, \mathcal{Or}$, and the initial configuration of the conclusion of the rule is inside the program point $\mu'$ immediately above $\mu$.

* $\mathbf{Conf}$ is the target configuration of a semantic rule. In rules (NewT), (LetT), (IfT1), (IfT2), (FindT1), (FindT2), (InsertT), (GetT1), (GetT2), and (EventT), the initial configuration of the rule is inside the program point $\mu'$ immediately above $\mu$. In rule (CxtT), the initial
configuration of the rule is inside the same program point $\mu$. In rule (DefinedYes), this rule is used to conclude assumptions of find, and the initial configuration of the find rule is inside the program point $\mu'$ immediately above $\mu$. In the rules for oracle definitions, if $\mu$ is the program point of an unchanged element of $Q$, the initial configuration of the rule is also inside $\mu$. This is sufficient for (Nil). If $\mu$ is the program point of a modified oracle, then for rules (Par), (Repl), and (NewOracle), the initial configuration of the rule is inside the program point $\mu'$ immediately above $\mu$, and for rule (DefOracle), the initial configuration of the rule is inside the same program point $\mu$. In the rules for oracle bodies other than (AttIO), (AttYield), (OracleCall), and (Return), $Q$ is unchanged, so if $\mu$ is the program point of an oracle declaration in $Q$, then the initial configuration of the rule is inside the same program point $\mu$. If $\mu$ is the program point of an oracle body not at the root of the stack, then the initial configuration of the rule is also inside the same program point $\mu$, because that part of the stack is unchanged. In rules (New), (Let), (If1), (If2), (Find1), (Find2), (Insert), (Get1), (Get2), (Event), and (Yield), if $\mu$ is the program point of an oracle body at the root of the stack, then the initial configuration of the rule is inside the program point $\mu'$ immediately above $\mu$. In rule (Ctx), the initial configuration of the rule is inside the same program point $\mu$.

In rules (OracleCall), (AttYield), and (AttIO), if $\mu$ is the program point of an oracle definition in $Q$, then the initial configuration of the rule is inside the same program point $\mu$. In rules (OracleCall) and (AttYield), if $\mu$ is the program point of $P'$, then the initial configuration of the rule is inside the program point $\mu'$ immediately above $\mu$, because $(\sigma', Q_0) \in S \subseteq Q$ and $\mu'$ is the program point of $Q_0$. Additionally, in rule (OracleCall), if $\mu$ is the program point of an oracle body in $(\sigma, P'_0) :: St$, then the initial configuration of the rule is inside the same program point $\mu$. In rule (AttIO), we have $(\sigma', Q_0) \in S \subseteq Q \uplus Q'$. If $(\sigma', Q_0) \in Q$ and $\mu$ is the program point of $P'$, then the initial configuration of the rule is inside the program point $\mu'$ immediately above $\mu$, as above because $\mu'$ is the program point of $Q_0$. If $(\sigma', Q_0) \in Q'$ and $\mu$ is the program point of $P'$, then $Q', Or'$ is inside the program point $\mu'$ immediately above $\mu$.

In rule (Return), if $\mu$ is the program point of an oracle definition in $Q$, then the initial configuration of the rule is inside the same program point $\mu$. If $\mu$ is the program point of an oracle definition in $Q'$, then the configuration $Q', Or'$ in the assumption of the rule is inside the same program point $\mu$. If $\mu$ is the program point of $P_1$, then the initial configuration of the rule is inside the program point $\mu'$ immediately above $\mu$ as $(\sigma', P_0)$ is in the stack and $\mu'$ is the program point of $P_0$. If $\mu$ is the program point of an oracle body in $St$, then the initial configuration of the rule is inside the same program point $\mu$.

Second property. Suppose that $Conf$ is inside $\mu$ and there is a program point $\mu'$ immediately above $\mu$ in $Q_0$. Let us show that there exists $Conf' \preceq_{Tr} Conf$ such that $Conf'$ is inside $\mu'$. The proof proceeds by well-founded induction on $\preceq_{Tr}$. The program point $\mu$ is not at the top of $Q_0$, so by the first property, there exists $Conf' \neq Conf$ such that $Conf' \preceq_{Tr} Conf$ and $Conf'$ is inside $\mu$ or inside $\mu'$. If $Conf'$ is inside $\mu$, we conclude by applying the induction hypothesis on $Conf'$. If $Conf'$ is inside $\mu'$, we have the result. By applying this property repeatedly, we obtain the second property. $\square$

**Lemma 7** Let $Tr$ be a trace of $Q_0$ for any $A \in \mathcal{B}\mathcal{B}$.

1. If $Conf = E, \sigma, C_m[\dots C_1[\mu^M]\dots]$, $T, \mu \in \mathcal{E}$ is the target configuration of a semantic rule in $Tr$, where $\mu$ is a program point in $Q_0, C_1, \dots, C_m$ are term contexts defined in Figure 7, and $\mu^M$ is not a subterm of $Q_0$, then the reduction that yields $Conf$ is obtained by $m$
applications of (CtxT) with contexts $C_m, \dots, C_1$ from a reduction with target configuration $E, \sigma, \mu^M, \mathcal{T}, \mu\mathcal{E}v$, itself proved by (CtxT).

2. If $\text{Conf} = E, (\sigma, C_0[C_m[\dots C_1[\mu^M]\dots]]) :: \text{St}, \mathcal{Q}, \text{Or}, \mathcal{T}, \mu\mathcal{E}v$ is the target configuration of a semantic rule in Tr, where $\mu$ is a program point in $Q_0$, $C_0$ is an oracle context defined in Figure 12, $C_1, \dots, C_m$ are term contexts defined in Figure 7, and $\mu^M$ is not a subterm of $Q_0$, then the reduction that yields Conf is obtained by one application of (Ctx) with context $C_0$ and $m$ applications of (CtxT) with contexts $C_m, \dots, C_1$ from a reduction with target configuration $E, \sigma, \mu^M, \mathcal{T}, \mu\mathcal{E}v$, itself proved by (CtxT).

**Proof** Property 1. This property is proved by induction of $m$. The reduction that yields Conf cannot be obtained by (NewT), (LetT), (IfT1), (IfT2), (FindT1), (FindT2), (InsertT), (GetT1), (GetT2), (EventT), (DefinedYes), because in this case, by Corollary 1, $C_m[\dots C_1[\mu^M]\dots]$ would be a subterm of $Q_0$, so $\mu^M$ would be a subterm of $Q_0$. So it is obtained by (CtxT). For $m=0$, this is enough to conclude. For $m > 0$, the rule (CtxT) is applied with context $C_m$. Indeed, since $\mu^M$ is not a value, the hole of the context cannot be after $C_{m-1}[\dots C_1[\mu^M]\dots]$ and, since $\mu^M$ is not a subterm of $Q_0$, the hole of the context cannot be before $C_{m-1}[\dots C_1[\mu^M]\dots]$. (If it were before, $C_{m-1}[\dots C_1[\mu^M]\dots]$ would not be in evaluation position in the initial configuration of rule (CtxT), so by Lemma 4, $C_{m-1}[\dots C_1[\mu^M]\dots]$ would be a subterm of $Q_0$.) Hence the reduction that yields Conf is obtained from a reduction that yields $E, \sigma, C_{m-1}[\dots C_1[\mu^M]\dots]$, $\mathcal{T}, \mu\mathcal{E}v$ by applying (CtxT) with context $C_m$. We conclude by applying the induction hypothesis.

Property 2. The reduction that yields Conf cannot be obtained by (New), (Let), (If1), (If2), (Find1), (Find2), (Insert), (Get1), (Get2), (Return), (Yield), (OracleCall), (AttYield), (AttIO), or (Event), because in this case, by Corollary 1, the oracle body of Conf would be a subprocess of $Q_0$ up to renaming of oracles, so $\mu^M$ would be a subterm of $Q_0$. Therefore, Conf is the target configuration of (Ctx). Furthermore, by the same reasoning as in Property 1, this rule is applied with context $C_0$. Hence the reduction that yields Conf is obtained from a reduction that yields $E, \sigma, C_m[\dots C_1[\mu^M]\dots]$, $\mathcal{T}, \mu\mathcal{E}v$ by applying (Ctx) with context $C_0$. We conclude by Property 1. □

**Lemma 8** Let Tr be a trace of $Q_0$ for any $\mathcal{A} \in \mathcal{BB}$.

1. If $\text{Conf} = E, (\sigma, \mu^P) :: \text{St}, \mathcal{Q}, \text{Or}, \mathcal{T}, \mu\mathcal{E}v$ is a configuration in Tr where $\mu$ is a program point in $Q_0$, then this configuration is derived in Tr from a configuration Conf' = $E'$, $(\sigma, \mu^P) :: \text{St}', \mathcal{Q}', \text{Or}', \mathcal{T}', \mu\mathcal{E}v'$ where $\mu^P$ is a subprocess of $Q_0$ up to renaming of oracles, by (Ctx) any number of times.

2. If $\text{Conf} = \{(\sigma, \mu^Q)\} \uplus \mathcal{Q}, \text{Or}$ is a configuration in Tr where $\mu$ is a program point in $Q_0$, then, possibly after swapping reductions in Tr, this configuration is derived from a configuration Conf' = $\{(\sigma, \mu^Q)\} \uplus \mathcal{Q}, \text{Or}$ where $\mu^Q$ is a subprocess of $Q_0$ up to renaming of oracles, by (DefOracle) any number of times.

3. If $\text{Conf} = E, (\sigma, C_0[C_m[\dots C_1[\mu^M]\dots]]) :: \text{St}, \mathcal{Q}, \text{Or}, \mathcal{T}, \mu\mathcal{E}v$ is a configuration in Tr where $\mu$ is a program point in $Q_0$, $C_0$ is an oracle context defined in Figure 12, and $C_1, \dots, C_m$ are term contexts defined in Figure 7, then we have

$$E', \sigma, \mu^M', \mathcal{T}', \mu\mathcal{E}v' \xrightarrow{p} t \dots \xrightarrow{p'} t' E, \sigma, \mu^M, \mathcal{T}, \mu\mathcal{E}v$$

by (CtxT) any number of times, where $\mu^M'$ is a subterm of $Q_0$ and in Tr, these reductions are in fact performed starting from a configuration Conf' = $E'$, $(\sigma, C_0[C_m[\dots C_1[\mu^M]\dots]])$, $\mathcal{Q}, \text{Or}, \mathcal{T}', \mu\mathcal{E}v'$ under one application of rule (Ctx) with context $C_0$ and $m$ applications of rule (CtxT) with contexts $C_m, \dots, C_1$.
4. If $Conf = E, \sigma, C_l[\dots C_1[\mu M]\dots], T, \mu\mathcal{E}v$ is a configuration in $Tr$ and $\mu$ is a program point in $Q_0$ where $C_1, \dots, C_l$ are term contexts defined in Figure 7, then we have

$$E', \sigma, \mu M', T', \mu\mathcal{E}v' \xrightarrow{p} t \dots \xrightarrow{p'} t' E, \sigma, \mu M, T, \mu\mathcal{E}v$$

by (CtxT) any number of times, where $\mu M'$ is a subterm of $Q_0$ and in $Tr$, these reductions are in fact performed starting

* from a configuration $Conf' = E', \sigma, C_m[\dots C_1[\mu M']\dots], T', \mu\mathcal{E}v'$ where $m \ge l, C_1, \dots, C_m$ are term contexts defined in Figure 7, under $m$ applications of (CtxT) with contexts $C_m, \dots, C_1$.

* or from a configuration $Conf' = E', (\sigma, C_0[C_m[\dots C_1[\mu M']\dots]]) :: St, Q, Or, T', \mu\mathcal{E}v'$ where $m \ge l, C_0$ is an oracle context defined in Figure 12, and $C_1, \dots, C_l$ are term contexts defined in Figure 7, under one application of (Ctx) with context $C_0$ and $m$ applications of (CtxT) with contexts $C_m, \dots, C_1$.

**Proof** Property 1. The proof proceeds by well-founded induction on $\leq_{Tr}$. The configuration $Conf$ cannot be initConfig($Q_0, A$) because $\mu$ is a program point in $Q_0$. Then, $Conf$ is the target configuration of some semantic rule. If $Conf$ is the target configuration of (New), (Let), (If1), (If2), (Find1), (Find2), (Insert), (Get1), (Get2), (OracleCall), (Return), (AttYield), (AttIO) or (Event), then by Corollary 1, $\mu P$ is a subprocess of $Q_0$ up to renaming of oracles, so the property holds with $Conf' = Conf$. If it is the target configuration of (Ctx), we conclude by applying the induction hypothesis to the initial configuration of this rule.

Property 2. The proof proceeds by well-founded induction on $\leq_{Tr}$. If $Conf = \{(\sigma_0, Q_0)\}$, $(\text{fo}(Q_0), \emptyset)$, then the property holds with $Conf' = Conf$, since $Q_0$ is a subprocess of $Q_0$. If $Conf$ is the initial configuration of the assumption of (Return) or (AttIO), then by Lemma 4, $Q$ is a subprocess of $Q_0$ up to renaming of oracles, since $Q$ occurs in non-evaluation position in the initial configuration of (Return) or (AttIO). So the property holds with $Conf' = Conf$. Otherwise, $Conf$ is the target configuration of a semantic rule.

* If that rule does not affect $Q$, then it is of the form $\{(\sigma, \mu Q)\} \uplus Q', Or' \rightsquigarrow \{(\sigma, \mu Q)\} \uplus Q, Or$. We apply the induction hypothesis to $\{(\sigma, \mu Q)\} \uplus Q', Or'$, so possibly after swapping reductions in $Tr$, we have $\{(\sigma, \mu Q')\} \uplus Q', Or' \rightsquigarrow^* \{(\sigma, \mu Q)\} \uplus Q', Or'$$ by (DefOracle) any number of times, where $\mu Q'$ is a subprocess of $Q_0$ up to renaming of oracles. By swapping reductions, we have $\{(\sigma, \mu Q')\} \uplus Q', Or' \rightsquigarrow \{(\sigma, \mu Q')\} \uplus Q, Or \rightsquigarrow^* \{(\sigma, \mu Q)\} \uplus Q, Or$, so we obtain the desired property with $Conf' = \{(\sigma, \mu Q')\} \uplus Q, Or$.

* Otherwise, that rule affects $Q$. If that rule is (Par), (Repl), or (NewOracle), then by Lemma 4, $Q$ is a subprocess of $Q_0$ up to renaming of oracles, since $Q$ occurs in non-evaluation position in the initial configuration of the rule. So the property holds with $Conf' = Conf$. If that rule is (DefOracle), then we obtain the result by induction hypothesis applied to the initial configuration of the rule.

Property 3. The proof proceeds by well-founded induction on $\leq_{Tr}$. The configuration $Conf$ cannot be initConfig($Q_0, A$) because $\mu$ is a program point in $Q_0$. Then, $Conf$ is the target configuration of some semantic rule. If $\mu M$ is a subterm of $Q_0$, then the property holds with $Conf' = Conf$. Otherwise, by Lemma 7, Property 2, the reduction that yields $Conf$ is obtained by one application of (Ctx) with context $C_0$ and $m$ applications of (CtxT) with contexts $C_m, \dots, C_1$ from a reduction with target configuration $E, \sigma, \mu M, T, \mu\mathcal{E}v$, itself proved by (CtxT). We obtain the desired property by applying the induction hypothesis to the configuration before this reduction step by (Ctx).
Property 4. The proof proceeds by well-founded induction on $\leq_T$. First case: Conf is the initial configuration of an assumption of a semantic rule. This rule cannot be a rule for find (in rules for find, the initial configuration of assumption is not inside a program point, because it evaluates the defined condition, not a term). In rules for get, (DefinedNo), and (DefinedYes), by Lemma 4, since the term in Conf occurs in non-evaluation position in the initial configuration of the rule, it is a subterm of $Q_0$, so $^\mu M$ is a subterm of $Q_0$. The property holds with $Conf' = Conf$. In (CxtT), we let $C_{l+1}$ be the context used in this rule, and we conclude by induction hypothesis applied to the initial configuration of this rule: $E, \sigma, C_{l+1}[C_l[\dots C_1[^\mu M]\dots]]$, $T, \mu\mathcal{E}v$. In (Cxt), we let $m = l$. The initial configuration of the rule is of the form $E, (\sigma, C_0[C_l[\dots C_1[^\mu M]\dots]])$, $Q, Or, T, \mu\mathcal{E}v$ for some process context $C_0$ defined in Figure 12. We conclude by applying Property 3 to that configuration.

Second case: Conf is the target configuration of a semantic rule. If $^\mu M$ is a subterm of $Q_0$, then the property holds with $Conf' = Conf$. Otherwise, by Lemma 7, Property 1, the reduction that yields Conf is obtained by $l$ applications of (CxtT) with contexts $C_l, \dots, C_1$ from a reduction with target configuration $E, \sigma, ^\mu M, T, \mu\mathcal{E}v$, itself proved by (CxtT). We apply the induction hypothesis to the initial configuration of the reduction that yields Conf, and we continue the reduction one more step by applying possibly (Cxt) with context $C_0$, (CxtT) $m$ times with contexts $C_m, \dots, C_1$ under the reduction with target configuration $E, \sigma, ^\mu M, T, \mu\mathcal{E}v$. This is also what happens in Tr. (By inspection of the rules, only the rule (Cxt) with context $C_0$ can reduce an oracle body $C_0[N]$, where $C_0$ is a process context defined in Figure 12; only the rule (CxtT) with context $C_j$ can reduce a term $C_j[N]$, where $C_j$ is a term context defined in Figure 7.) $\square$

### 2.4.3 Each Variable is Defined at Most Once

In this section, we show that Invariant 1 implies that each array cell is assigned at most once during the execution of a process.

We define the multiset of variable accesses that may be defined by a term or a process (given the replication indices fixed by a mapping sequence $\sigma$) as follows:

$$Defined(\sigma, ^\mu i) = \emptyset$$

$$Defined(\sigma, ^\mu x[M_1, \dots, M_m]) = \bigcup_{j=1}^{m} Defined(\sigma, M_j)$$

$$Defined(\sigma, ^\mu f(M_1, \dots, M_m)) = \bigcup_{j=1}^{m} Defined(\sigma, M_j)$$

$$Defined(\sigma, ^\mu x[i] \stackrel{R}{\leftarrow} T; N) = \{x[\sigma(i)]\} \cup Defined(\sigma, N)$$

$$Defined(\sigma, ^\mu \text{let } x[i] : T = M \text{ in } N) = \{x[\sigma(i)]\} \cup Defined(\sigma, M) \cup Defined(\sigma, N)$$

$$Defined(\sigma, ^\mu \text{if } M \text{ then } N \text{ else } N') = Defined(M) \cup \max(Defined(N), Defined(N'))$$

$$Defined(\sigma, ^\mu \text{find}[\text{unique?}] (\bigoplus_{j=1}^{m} \tilde{u}_j[i] = \tilde{u}_j \leq \tilde{n}_j \text{ suchthat } Defined(\tilde{M}_j) \land M_j \text{ then } N_j) \text{ else } N) = \\ \max(\max_{j=1}^{m} \max_{\tilde{a} \leq \tilde{n}_j} Defined(\sigma[i_j \mapsto \tilde{a}], M_j), \max_{j=1}^{m} \{\tilde{u}_j[\sigma(i)]\} \cup Defined(\sigma, N_j), Defined(\sigma, N))$$

$$Defined(\sigma, ^\mu \text{insert } Tbl(M_1, \dots, M_l; N) = \bigcup_{j=1}^{l} Defined(\sigma, M_j) \cup Defined(\sigma, N)$$
$$
\text{Defined}(\sigma, \mu \text{get}[\text{unique} ?] \text{Tbl}(x_1[\tilde{i}] : T_1, \dots, x_l[\tilde{i}] : T_l) \text{ suchthat } M \text{ in } N \text{ else } N') =
\max(\{x_j[\sigma(\tilde{i})] | j \le l\} \uplus \max(\text{Defined}(\sigma, M), \text{Defined}(\sigma, N)), \text{Defined}(\sigma, N'))
$$

$$
\text{Defined}(\sigma, \mu \text{event } e(M_1, \dots, M_l; N)) = \bigcup_{j=1}^{l} \text{Defined}(\sigma, M_j) \uplus \text{Defined}(\sigma, N)
$$

$$
\text{Defined}(\sigma, \mu \text{event\_abort } e) = \emptyset
$$

$$
\text{Defined}(\sigma, a) = \text{Defined}(\sigma, \text{event\_abort}(\mu, \tilde{a}) : e) = \emptyset
$$

$$
\text{Defined}(\sigma, \mu 0) = \emptyset
$$

$$
\text{Defined}(\sigma, \mu(Q_1 | Q_2)) = \text{Defined}(\sigma, Q_1) \uplus \text{Defined}(\sigma, Q_2)
$$

$$
\text{Defined}(\sigma, \mu \text{foreach } i \le n \text{ do } Q) = \bigcup_{a \in [1, n]} \text{Defined}(\sigma[i \mapsto a], Q)
$$

$$
\text{Defined}(\sigma, \mu \text{newOracle } O; Q) = \text{Defined}(\sigma, Q)
$$

$$
\text{Defined}(\sigma, \mu O[\tilde{i}](x[\tilde{i}] : T) := P) = \{x[\sigma(\tilde{i})]\} \uplus \text{Defined}(\sigma, P)
$$

$$
\text{Defined}(\sigma, \mu \text{return } (M); Q) = \text{Defined}(\sigma, M) \uplus \text{Defined}(\sigma, Q)
$$

$$
\text{Defined}(\sigma, \mu \text{let } x[\tilde{i}] : T = O[M_1, \dots, M_l, ?u_1[\tilde{i}] \le n_1, \dots, ?u_m[\tilde{i}] \le n_m](N) \text{ in } P \text{ else } P') =
\bigcup_{j=1}^{l} \text{Defined}(M_j) \uplus \{u_j[\sigma(\tilde{i})] | j \le m\} \uplus \max(\{x[\sigma(\tilde{i})]\} \uplus \text{Defined}(\sigma, P), \text{Defined}(\sigma, P'))
$$

$$
\text{Defined}(\sigma, \mu x[\tilde{i}] \stackrel{R}{\leftarrow} T; P) = \{x[\sigma(\tilde{i})]\} \uplus \text{Defined}(\sigma, P)
$$

$$
\text{Defined}(\sigma, \mu \text{let } x[\tilde{i}] : T = M \text{ in } P) = \{x[\sigma(\tilde{i})]\} \uplus \text{Defined}(\sigma, M) \uplus \text{Defined}(\sigma, P)
$$

$$
\text{Defined}(\sigma, \mu \text{if } M \text{ then } P \text{ else } P') = \text{Defined}(M) \uplus \max(\text{Defined}(P), \text{Defined}(P'))
$$

$$
\text{Defined}(\sigma, \mu \text{find}[\text{unique} ?] (\bigoplus_{j=1}^{m} \tilde{u}_j[\tilde{i}] = \tilde{i}_j \le \tilde{n}_j \text{ suchthat } \text{defined}(\tilde{M}_j) \wedge M_j \text{ then } P_j) \text{ else } P) =
\max\left(\max_{j=1}^{m} \max_{\tilde{a} \le \tilde{n}_j} \text{Defined}(\sigma[\tilde{i}_j \mapsto \tilde{a}], M_j), \max_{j=1}^{m} \{\tilde{u}_j[\sigma(\tilde{i})]\} \uplus \text{Defined}(\sigma, P_j), \text{Defined}(\sigma, P)\right)
$$

$$
\text{Defined}(\sigma, \mu \text{insert } \text{Tbl}(M_1, \dots, M_l; P)) = \bigcup_{j=1}^{l} \text{Defined}(\sigma, M_j) \uplus \text{Defined}(\sigma, P)
$$

$$
\text{Defined}(\sigma, \mu \text{get}[\text{unique} ?] \text{Tbl}(x_1[\tilde{i}] : T_1, \dots, x_l[\tilde{i}] : T_l) \text{ suchthat } M \text{ in } P \text{ else } P') =
\max(\{x_j[\sigma(\tilde{i})] | j \le l\} \uplus \max(\text{Defined}(\sigma, M), \text{Defined}(\sigma, P)), \text{Defined}(\sigma, P'))
$$

$$
\text{Defined}(\sigma, \mu \text{event } e(M_1, \dots, M_l; P)) = \bigcup_{j=1}^{l} \text{Defined}(\sigma, M_j) \uplus \text{Defined}(\sigma, P)
$$

$$
\text{Defined}(\sigma, \mu \text{event\_abort } e) = \emptyset
$$

$$
\text{Defined}(\sigma, \text{abort}) = \emptyset
$$

$$
\text{Defined}(\sigma, \text{yield}) = \emptyset
$$

Notice that, by Invariant 5, the terms $\tilde{M}_j$ in defined conditions of find do not define any variable. By Invariant 3, the variables defined in conditions of find and get can be considered as defined temporarily only during the evaluation of the considered condition. Given a configuration $Conf = E, \sigma, N, \mathcal{T}, \mu\mathcal{E}v$ or $Conf = E, St, Q, Or, \mathcal{T}, \mu\mathcal{E}v$, we denote by $E_{Conf}$ the environment $E$ in configuration $Conf$. For $Conf = Q, Or, E_{Conf}$ is empty. We define

$$
\text{Defined}^{\text{Fut}}(E, \sigma, M, \mathcal{T}, \mu\mathcal{E}v) = \text{Defined}(\sigma, M)
$$
$$ \mathit{Defined}^{\mathit{Fut}}(Q, Or) = \biguplus_{(\sigma, Q) \in Q} \mathit{Defined}(\sigma, Q) $$

$$ \mathit{Defined}^{\mathit{Fut}}(E, St, Q, Or, T, \mu\mathit{Ev}) = \biguplus_{(\sigma, P) \in St} \mathit{Defined}(\sigma, P) \uplus \biguplus_{(\sigma, Q) \in Q} \mathit{Defined}(\sigma, Q) $$

$$ \mathit{Defined}(\mathit{Conf}) = \mathrm{Dom}(E_{\mathit{Conf}}) \uplus \mathit{Defined}^{\mathit{Fut}}(\mathit{Conf}). $$

**Invariant 9 (Single definition, for executing games)** The semantic configuration Conf (which can be E, σ, M, T, μEv or Q, Or or E, St, Q, Or, T, μEv) satisfies Invariant 9 if and only if Defined(Conf) does not contain duplicate elements.

**Lemma 9** Let Tr be trace of Q₀ for any A ∈ BB. If Q₀ satisfies Invariant 1, then all semantic configurations in the derivation of Tr satisfy Invariant 9.

**Proof sketch** We first show that, for all program points μ in Q₀, if Dom(σ) = Iμ are the current replication indices at μ and the process or term Q at μ satisfies Invariant 1, then all elements of Defined(σ, Q) are of the form x[~a] where x ∈ vardef(Q) and Im(σ) is a prefix of ~a. The proof proceeds by induction on Q. At the definition of a variable x[i], x[σ(~i)] is added to Defined(σ, Q) and we have x ∈ vardef(Q); by Invariant 1, ~i are the current replication indices at that definition, so σ(~i) = Im(σ). All recursive calls Defined(σ', μ'Q') consider an extension σ' of σ and a subprocess or subterm Q' of Q (so vardef(Q') ⊆ vardef(Q)) such that Dom(σ') = Iμ' are the current replication indices at μ'.

Next, we show that, for all program points μ, if Dom(σ) = Iμ are the current replication indices at μ and the process or term Q at μ satisfies Invariant 1, then Defined(σ, Q) does not contain duplicate elements. The proof proceeds by induction on Q. All multiset unions in the computation of Defined(σ, Q) are disjoint unions by the property above, because either they use different extensions of σ (case of replication) or they use disjoint variable definitions or subprocesses or subterms in the same branch of find, if, get, or oracle call, which must define different variables by Invariant 1.

We show by induction on the derivations that, if Conf $\xrightarrow{p}$$_t$ Conf', then Defined(Conf) ⊇ Defined(Conf') and for all semantic configurations Conf'' in the derivation of Conf $\xrightarrow{p}$$_t$ Conf', Defined(Conf) ⊇ Defined(Conf''), and similarly with $\rightsquigarrow$ instead of $\xrightarrow{p}$$_t$.

The result follows: since Q₀ satisfies Invariant 1, Defined(σ₀, Q₀) does not contain duplicate elements, where σ₀ is the empty mapping sequence. Then {{(σ₀, Q₀)}, (fo(Q₀), ∅)} satisfies Invariant 9 and so do reduce({(σ₀, Q₀)}, (fo(Q₀), ∅)), initConfig(Q₀, A), and the other configurations of Tr. □

**Corollary 2** If Q₀ satisfies Invariant 1, then each variable that is not defined in a condition of find or get is defined at most once for each value of its array indices in a trace of Q₀ for any A ∈ BB.

**Proof** Let x be the considered variable and Tr be the considered trace of Q₀. The only semantic rules that can add x[~a] to the environment E are (NewT), (LetT), (FindT1), (GetT1), (New), (Let), (Find1), (Get1), (AttYield), (AttIO), (OracleCall) and (Return). By Corollary 1, the target term or process of these rules is a subterm or subprocess of Q₀ up to renaming of oracles. Hence, the target configuration Conf' of these rules is at some program point μ in Tr. By hypothesis, x is not defined in conditions of find or get, so μ is not inside the condition of find or get in Q₀, so by Lemma 5, the configuration Conf' is not in the derivation of an assumption of a rule for find or get.
In order to derive a contradiction, assume that two transitions $Conf_1 \xrightarrow{p_1} Conf'_1$ and $Conf_2 \xrightarrow{p_2} Conf'_2$ inside $Tr$ define the same variable $x[\tilde{a}]$.

* First case: one transition happens before the other, for instance $Conf'_1 \preceq_T Conf_2$. (The case $Conf'_2 \preceq_T Conf_1$ is symmetric.) Since $Conf_1 \xrightarrow{p_1} Conf'_1$ defines $x[\tilde{a}]$, we have $x[\tilde{a}] \in \text{Dom}(E_{Conf'_1})$. Since $Conf'_1$ is not in the derivation of an assumption of a rule for find or get, by Lemma 3, $E_{Conf_2}$ extends $E_{Conf'_1}$, so $x[\tilde{a}] \in \text{Dom}(E_{Conf_2})$. Moreover, since $Conf_2 \xrightarrow{p_2} Conf'_2$ defines $x[\tilde{a}]$, we have $x[\tilde{a}] \in \text{Defined}^{\text{Fut}}(Conf_2)$, by inspecting all rules that add elements to the environment. Therefore $\text{Defined}(Conf_2) = \text{Dom}(E_{Conf_2}) \uplus \text{Defined}^{\text{Fut}}(Conf_2)$ contains twice $x[\tilde{a}]$. Contradiction with Invariant 9.

* Second case: the transitions cannot be ordered. By definition of $\preceq_T$, this can happen only when a semantic rule uses several derivations for its assumptions, which happens only in rules for find or get. Contradiction.

That concludes the proof. □

Variables defined in conditions of get may be defined several times, once for each element of the table that is tested. Variables defined in conditions of find may be defined several times in case the same variable is used in several branches of the same find. (We use the indices of the find as indices of the variables defined in the condition, so when we evaluate several times the condition of a certain branch of a find, we use variables with different indices.) In Section 2.7, we define properties that exclude these situations (Properties 3 and 4), and we prove in Lemma 29 that every variable is defined at most once for each value of its indices when these properties are satisfied.

### 2.4.4 Each Oracle is defined at most once

Similarly to the variable definition case, we can show that Invariant 7 implies that each oracle is defined at most once during the execution of a process. This ensures that for every oracle call, a unique corresponding oracle is potentially available. We generalize the previous $Defined^O$ definition of Invariant 7 to also take into account the replication indices fixed by a mapping sequence $\sigma$ as follows:

$$Defined_p^O(\sigma, \mu 0) = \emptyset$$

$$Defined_p^O(\sigma, \mu(Q_1 | Q_2)) = Defined_p^O(\sigma, Q_1) \uplus Defined_p^O(\sigma, Q_2)$$

$$Defined_p^O(\sigma, \mu \text{foreach } i \le n \text{ do } Q) = \bigcup_{a \in [1, n]} Defined_p^O(\sigma[i \mapsto a], Q)$$

$$Defined_p^O(\sigma, \mu \text{newOracle } O; Q) = Defined_p^O(\sigma, Q) \setminus \{O[\tilde{i}] | k \in \mathbb{N}, \tilde{i} \in \mathbb{N}^k\}$$

$$Defined_p^O(\sigma, \mu O[\tilde{i}](x[\tilde{i}] : T) := P) = \{O[\sigma(\tilde{i})]\} \uplus Defined_p^O(\sigma, P)$$

$$Defined_p^O(\sigma, \mu C[Q_1, \dots, Q_k]) = \max_{j=1}^k Defined_p^O(\sigma, Q_j)$$

Here, similarly to the definition of Invariant 7, $C$ is a context restricted to oracle body constructs only. We lift $Defined_p^O$ to configurations in a similar fashion to Defined, as:

$$Defined_p^O(Q, Or) = \bigcup_{(\sigma, Q) \in \mathcal{Q}} Defined_p^O(\sigma, Q)$$

$$Defined_p^O(E, St, Q, Or, T, \mu \mathcal{E}v) = \bigcup_{(\sigma, P) \in St} Defined_p^O(\sigma, P) \uplus \bigcup_{(\sigma, Q) \in \mathcal{Q}} Defined_p^O(\sigma, Q)$$
**Invariant 10 (Single definition, for executing games)** The semantic configuration Conf (which can be Q, Or or E, St, Q, Or, T, μEv) satisfies Invariant 10 if and only if $Defined_p^O(Conf)$ does not contain duplicate elements.

**Lemma 10** Let Tr be trace of $Q_0$ for any $A \in \mathcal{BB}$. If $Q_0$ satisfies Invariant 7, then all semantic configurations in the derivation of Tr satisfy Invariant 10.

We omit the proof, which is similar to the one of Lemma 9. The core difference is that $Defined_p^O$ does not directly diminish over the evolution of configurations, as newOracle O introduces new definitions. We remark that however, $Defined_p^O \cap Or_{pub}$ diminishes for all rules, and by construction, a newOracle O command introduces new oracle definitions that are distinct from all existing ones.

### 2.4.5 Variables are Defined Before Being Used

In this section, we show that Invariant 2 implies that all variables are defined before being used. In order to show this property, we use the following invariant:

**Invariant 11 (Defined variables, for executing games)** The semantic configuration $E, St, Q, Or, T, \mu Ev$ satisfies Invariant 11 if and only if every occurrence of a variable access $x[M_1, \dots, M_m]$ in $St$ or $Q$ is either

1. present in $Dom(E)$: if $x[M_1, \dots, M_m]$ occurs in a process $P'$ for $(\sigma', P') \in St \cup Q$, then for all $j \le m$, $E, \sigma', M_j \vdash a_j$ and $x[a_1, \dots, a_m] \in Dom(E)$;

2. or syntactically under the definition of $x[M_1, \dots, M_m]$ (in which case for all $j \le m$, $M_j$ is a constant or variable replication index);

3. or in a defined condition in a find process or term;

4. or in $M'_j$ in a process or term of the form find ($\bigoplus_{j=1}^{m''} \tilde{u}_j[\tilde{i}] = \tilde{i}_j \le \tilde{n}_j$ such that $defined(M'_{j1}, \dots, M'_{j_l}) \wedge M'_j$ then $P_j$) else $P$ where for some $k \le l_j$, $x[M_1, \dots, M_m]$ is a subterm of $M'_{jk}$.

5. or in $P_j$ in a process or term of the form find ($\bigoplus_{j=1}^{m''} \tilde{u}_j[\tilde{i}] = \tilde{i}_j \le \tilde{n}_j$ such that $defined(M'_{j1}, \dots, M'_{j_l}) \wedge M'_j$ then $P_j$) else $P$ where for some $k \le l_j$, there is a subterm $N$ of $M'_{jk}$ such that $N\{\tilde{u}_j[\tilde{i}]/\tilde{i}_j\} = x[M_1, \dots, M_m]$.

Similarly, $E, \sigma, M, T, \mu Ev$ satisfies Invariant 11 if and only if every occurrence of a variable access $x[M_1, \dots, M_m]$ in $M$ either is present in $Dom(E)$ (for all $j \le m$, $E, \sigma, M_j \vdash a_j$ and $x[a_1, \dots, a_m] \in Dom(E)$) or satisfies one of the last four conditions above.

$E, \sigma, defined(M'_1, \dots, M'_l) \wedge M, T, \mu Ev$ satisfies Invariant 11 if and only if every occurrence of a variable access $x[M_1, \dots, M_m]$ in $M$ either is a subterm of $M'_1, \dots, M'_l$, or is present in $Dom(E)$ (for all $j \le m$, $E, \sigma, M_j \vdash a_j$ and $x[a_1, \dots, a_m] \in Dom(E)$) or satisfies one of the last four conditions above.

Recall that, by Invariants 2 and 5, the terms of all variable accesses $x[M_1, \dots, M_m]$ are simple. That is why we can evaluate them by $E, \sigma', M_j \vdash a_j$.

**Lemma 11** If $Q_0$ satisfies Invariant 2, then initConfig($Q_0, A$) satisfies Invariant 11.

**Lemma 12** Let $M$ be a simple term. If $E, \sigma, M \vdash a$, then for all subterms $x[M_1, \dots, M_m]$ of $M$, for all $j' \le m$, $E, \sigma, M_{j'} \vdash a_{j'}$ and $x[a_1, \dots, a_m]$ is in $Dom(E)$.
**Proof sketch** By induction on $M$. $\square$

**Lemma 13** Let $N, M$ be simple terms. If $E, \sigma[i \mapsto a'], N \Downarrow a$ and $E, \sigma, M \Downarrow a'$, then we have $E, \sigma, N\{M/i\} \Downarrow a$.

**Proof sketch** By induction on $N$. $\square$

**Lemma 14** If $E, \sigma, M, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p} t E', \sigma', M', \mathcal{T}', \mu\mathcal{E}v'$ and $E, \sigma, M, \mathcal{T}, \mu\mathcal{E}v$ satisfies Invariant 11, then so does $E', \sigma', M', \mathcal{T}', \mu\mathcal{E}v'$.

If $E, \sigma, \text{defined}(M_1, \dots, M_m) \wedge M, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p} t E', \sigma', M', \mathcal{T}', \mu\mathcal{E}v'$ and $E, \sigma, \text{defined}(M_1, \dots, M_m) \wedge M, \mathcal{T}, \mu\mathcal{E}v$ satisfies Invariant 11, then so does $E', \sigma', M', \mathcal{T}', \mu\mathcal{E}v'$.

If $E, St, Q, \mathcal{Or}, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p} t E', St', Q', \mathcal{Or}', \mathcal{T}', \mu\mathcal{E}v'$ and $E, St, Q, \mathcal{Or}, \mathcal{T}, \mu\mathcal{E}v$ satisfies Invariant 11, then so does $E', St', Q', \mathcal{Or}', \mathcal{T}', \mu\mathcal{E}v'$.

Moreover, if the rules that define $E, \sigma, M, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p} t E', \sigma', M', \mathcal{T}', \mu\mathcal{E}v'$ (respectively $E, \sigma, \text{defined}(M_1, \dots, M_m) \wedge M, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p} t E', \sigma', M', \mathcal{T}', \mu\mathcal{E}v'$ or $E, St, Q, \mathcal{Or}, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p} t E', St', Q', \mathcal{Or}', \mathcal{T}', \mu\mathcal{E}v'$) require as assumption $E'', \sigma'', M'', \mathcal{T}'', \mu\mathcal{E}v'' \xrightarrow{p} t \dots$ or $E'', \sigma'', \text{defined}(M_1'', \dots, M_m'') \wedge M'', \mathcal{T}'', \mu\mathcal{E}v'' \xrightarrow{p} t \dots$, and the initial configuration $E, \sigma, M, \mathcal{T}, \mu\mathcal{E}v$ (resp. $E, \sigma, \text{defined}(M_1, \dots, M_m) \wedge M, \mathcal{T}, \mu\mathcal{E}v$ or $E, St, Q, \mathcal{Or}, \mathcal{T}, \mu\mathcal{E}v$) satisfies Invariant 11, then so does the initial configuration of the assumption, $E'', \sigma'', M'', \mathcal{T}'', \mu\mathcal{E}v''$ or $E'', \sigma'', \text{defined}(M_1'', \dots, M_m'') \wedge M'', \mathcal{T}'', \mu\mathcal{E}v''$.

**Proof sketch** The proof proceeds by induction following the definition of $\xrightarrow{p} t$. We just sketch the main arguments.

If $x[M_1, \dots, M_m]$ is in the second case of Invariant 11, and we execute the definition of $x[M_1, \dots, M_m]$, then for all $j \le m$, $M_j$ is a variable replication index and $x[\sigma(M_1), \dots, \sigma(M_m)]$ is added to $\text{Dom}(E)$ by rules (NewT), (LetT), (FindT1), (GetT1), (New), (Let), (Find1), (AttYield), (AttIO), (OracleCall), (Return) or (Get1) so it moves to the first case of Invariant 11.

If $x[M_1, \dots, M_m]$ is in the third case of Invariant 11, and we execute the corresponding find, this access to $x$ simply disappears.

If $x[M_1, \dots, M_m]$ is in the fourth case of Invariant 11, and we execute the find, then $x[M_1, \dots, M_m]$ is a subterm of $M'_{jk}$ for some $j \le m''$ and $k \le l_j$. Therefore, the initial configuration of the assumption $E, \sigma[\tilde{i}_j \mapsto \tilde{a}], D_j \wedge M'_j, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p_{k'}} E'', \sigma', r_{k'}, \mathcal{T}, \mu\mathcal{E}v$ with $D_j \wedge M'_j = \text{defined}(M'_{j1}, \dots, M'_{jl_j}) \wedge M'_j$ and $\sigma' = \sigma[\tilde{i}_j \mapsto \tilde{a}]$ also satisfies Invariant 11. In case this assumption is reduced by (DefinedYes), we have $E, \sigma', M'_{jk}, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{1^*} E, \sigma', a_{jk}, \mathcal{T}, \mu\mathcal{E}v$, that is, $E, \sigma', M'_{jk} \Downarrow a_{jk}$. Therefore, by Lemma 12, for all $j' \le m$, $E, \sigma', M'_{j'}, \mathcal{Downarrow} a_{j'}$ and $x[a_1, \dots, a_m]$ is in $\text{Dom}(E)$. So $x[M_1, \dots, M_m]$ moves to the first case of Invariant 11 in $E, \sigma', M'_{j'}, \mathcal{T}, \mu\mathcal{E}v$ after reduction by (DefinedYes).

If $x[M_1, \dots, M_m]$ is in the last case of Invariant 11, and we execute the find selecting branch $j$ by (FindT1) or (Find1), then there is a subterm $N$ of $M'_{jk}$ for some $k \le l_j$ such that $N\{\tilde{u}_j[\tilde{i}]/\tilde{i}_j\} = x[M_1, \dots, M_m]$. By hypothesis of (FindT1) or (Find1), we have $E, \sigma[\tilde{i}_j \mapsto \tilde{a}], D_j \wedge M'_j, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p_{k'}} E, \sigma', r_{k'}, \mathcal{T}, \mu\mathcal{E}v$ where $r_{k'} = \text{true}$, $v_0 = (j, \tilde{a}) \in S$, $D_j \wedge M'_j = \text{defined}(M'_{j1}, \dots, M'_{jl_j}) \wedge M'_j$, and $\sigma' = \sigma[\tilde{i}_j \mapsto \tilde{a}]$. This assumption cannot reduce by (DefinedNo) because the result is true, so it reduces by (DefinedYes). Therefore, we have $E, \sigma', M'_{jk}, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{1^*} E, \sigma', a, \mathcal{T}, \mu\mathcal{E}v$ for some $a$, that is, $E, \sigma', M'_{jk} \Downarrow a$. The term $N = x[N_1, \dots, N_m]$ is a subterm of $M'_{jk}$. Therefore, by Lemma 12, for all $j' \le m$, $E, \sigma', N_{j'}, \mathcal{Downarrow} a_{j'}$ and $x[a_1, \dots, a_m]$ is in
Dom(E). Moreover, the resulting environment $E'$ is an extension of E, so a fortiori for all $j' \le m$, $E'$, $\sigma'$, $N_{j'} \triangleleft a_{j'}$ and $x[a_1, \dots, a_m]$ is in Dom(E'). We have for all $j' \le m$, $M_{j'} = N_{j'}\{\tilde{u}_j[i]/\tilde{u}_j\}$, $E'(\tilde{u}_j[i]) = \tilde{a}'$, and $\sigma'(\tilde{u}_j) = \tilde{a}'$, so by Lemma 13, for all $j' \le m$, $E'$, $\sigma$, $M_{j'} \triangleleft a_{j'}$ and $x[a_1, \dots, a_m]$ is in Dom(E'). So $x[M_1, \dots, M_m]$ also moves to the first case of Invariant 11.

In all other cases, the situation remains unchanged. For context rules, this is because, in the allowed contexts, the hole is never under a defined condition. □

Therefore, if $Q_0$ satisfies Invariant 2, then in traces of $Q_0$, the test $x[a_1, \dots, a_m] \in \text{Dom}(E)$ in rule (Var) always succeeds, except when the considered term occurs in a defined condition of a find.

Indeed, consider an application of rule (Var), where the array access $x[M_1, \dots, M_m]$ is not in a defined condition of a find. Then, this array access is not under any variable definition or find, so it is present in Dom(E): for all $j \le m$, $E$, $\sigma$, $M_j \triangleleft a_j$ and $x[a_1, \dots, a_m] \in \text{Dom}(E)$. Hence, the test $x[a_1, \dots, a_m] \in \text{Dom}(E)$ succeeds.

### 2.4.6 Typing

In this section, we show that our type system is compatible with the semantics of the oracles, that is, we define a notion of typing for semantic configurations and show that typing is preserved by reduction (subject reduction). Finally, the property that semantic configurations are well-typed shows that certain conditions in the semantics always hold.

We use the following definitions:

* $\mathcal{E} \vdash E$ if and only if $E(x[a_1, \dots, a_m]) = a$ implies $\mathcal{E}(x) = T_1 \times \dots \times T_m \to T$ with for all $j \le m$, $a_j \in T_j$ and $a \in T$.

* We define $\mathcal{E} \vdash P : T$, $\mathcal{E} \vdash Q$, and $\mathcal{E} \vdash M : T$ as in Section 2.3, with the additional rules $\mathcal{E} \vdash a : T$ if and only if $a \in T$, $\mathcal{E} \vdash \text{event_abort}(\mu, \tilde{a}) : e : T$ for all $T$, and $\mathcal{E} \vdash \text{abort} : T$ for all $T$. (These rules are useful to type evaluated terms and processes.)

* $\mathcal{E} \vdash (\sigma, P) : T$ if and only if $\mathcal{E}[i_1 \mapsto [1, n_1], \dots, i_m \mapsto [1, n_m]] \vdash P : T$ and for all $j \le m$, $\sigma(i_j) \in [1, n_j]$ for some $n_1, \dots, n_m$, where $\text{Dom}(\sigma) = [i_1, \dots, i_m]$. The judgments $\mathcal{E} \vdash (\sigma, M) : T$ and $\mathcal{E} \vdash (\sigma, Q)$ are defined in the same way.

* $\mathcal{E} \vdash (\sigma, P) : T \mapsto T'$ if and only if $\mathcal{E} \vdash (\sigma, P) : T'$ and P is of the form $\text{let } x[i] : T = O[M_1, \dots, M_l](N)$ in $P_1 \text{ else } P_2$.

* $\mathcal{E} \vdash \mathcal{T}$ if and only if $\text{Tbl}(a_1, \dots, a_m) \in \mathcal{T}$ implies $\text{Tbl} : T_1 \times \dots \times T_m$ with for all $j \le m$, $a_j \in T_j$.

* $\mathcal{E} \vdash \mu\mathcal{E}v$ if and only if $(\mu, \tilde{a}) : e(a_1, \dots, a_m) \in \mu\mathcal{E}v$ implies $e : T_1 \times \dots \times T_m$ with for all $j \le m$, $a_j \in T_j$.

* $\mathcal{E} \vdash E$, $(\sigma_0, P_0) :: \dots :: (\sigma_m, P_m) :: \mathcal{A}, \mathcal{Q}, \mathcal{Or}, \mathcal{T}, \mu\mathcal{E}v$ if and only if $\mathcal{E} \vdash E$, $(\sigma_0, P_0) : T_0$, for all $1 \le i \le m$, $\mathcal{E} \vdash (\sigma_i, P_i) : T_{i-1} \mapsto T_i$, $\mathcal{E} \vdash \mathcal{T}$, $\mathcal{E} \vdash \mu\mathcal{E}v$, and for all $(\sigma', Q) \in \mathcal{Q}$, $\mathcal{E} \vdash (\sigma', Q)$.

* $\mathcal{E} \vdash \mathcal{Q}, \mathcal{Or}$ if and only if for all $(\sigma', Q) \in \mathcal{Q}$, $\mathcal{E} \vdash (\sigma', Q)$.

* $\mathcal{E} \vdash E$, $\sigma$, $M : T$, $\mathcal{T}$, $\mu\mathcal{E}v$ if and only if $\mathcal{E} \vdash E$, $\mathcal{E} \vdash (\sigma, M) : T$, $\mathcal{E} \vdash \mathcal{T}$, and $\mathcal{E} \vdash \mu\mathcal{E}v$.

**Lemma 15** If $\mathcal{E} \vdash E$, $\sigma$, $M : T$, $\mathcal{T}$, $\mu\mathcal{E}v$ and $E$, $\sigma$, $M$, $\mathcal{T}$, $\mu\mathcal{E}v \stackrel{p}{\to}_t E'$, $\sigma'$, $M'$, $\mathcal{T}'$, $\mu\mathcal{E}v'$, then $\mathcal{E} \vdash E'$, $\sigma'$, $M' : T$, $\mathcal{T}'$, $\mu\mathcal{E}v'$.

So, $\mathcal{E} \vdash E$, $\sigma$, $M : T$, $\mathcal{T}$, $\mu\mathcal{E}v$ and $E$, $\sigma$, $M$, $\mathcal{T}$, $\mu\mathcal{E}v \stackrel{p}{\to}_t E'$, $\sigma'$, $a$, $\mathcal{T}'$, $\mu\mathcal{E}v'$, then $\mathcal{E} \vdash E'$, $\sigma'$, $a : T$, $\mathcal{T}'$, $\mu\mathcal{E}v'$.
**Proof sketch** By induction on the derivation of $E, \sigma, M, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p} {}_t E', \sigma', M', \mathcal{T}', \mu\mathcal{E}v'$. $\square$

**Lemma 16** If $\mathcal{E} \vdash Q, \mathcal{O}r$ and $Q, \mathcal{O}r \rightsquigarrow Q', \mathcal{O}r'$, then $\mathcal{E} \vdash Q', \mathcal{O}r'$.
So, if $\mathcal{E} \vdash Q, \mathcal{O}r$, then $\mathcal{E} \vdash \text{reduce}(Q, \mathcal{O}r)$.

**Proof sketch** By cases on the derivation of $Q, \mathcal{O}r \rightsquigarrow Q', \mathcal{O}r'$. In the case of the replication, we have $\mathcal{E} \vdash (\sigma, \text{foreach } i \le n \text{ do } Q)$, so $\mathcal{E}[i_1 \mapsto [1, n_1], \dots, i_m \mapsto [1, n_m]] \vdash \text{foreach } i \le n \text{ do } Q$ and for all $j \le m$, $\sigma(i_j) \in [1, n_j]$ for some $n_1, \dots, n_m$, where $\text{Dom}(\sigma) = [i_1, \dots, i_m]$. By (TRepl), $\mathcal{E}[i_1 \mapsto [1, n_1], \dots, i_m \mapsto [1, n_m], i \mapsto [1, n]] \vdash Q$, so $\mathcal{E} \vdash (\sigma[i \mapsto a], Q)$ for $a \in [1, n]$. $\square$

**Lemma 17** If $\mathcal{E} \vdash Q_0$, then $\mathcal{E} \vdash \text{initConfig}(Q_0, \mathcal{A})$.

**Proof sketch** By Lemma 16 and the previous definitions. $\square$

**Lemma 18 (Subject reduction)** If $\mathcal{E} \vdash E, St, Q, \mathcal{O}r, \mathcal{T}, \mu\mathcal{E}v$ and $E, St, Q, \mathcal{O}r, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p} {}_t E'$, $St', Q', \mathcal{O}r', \mathcal{T}', \mu\mathcal{E}v'$, then $\mathcal{E} \vdash E', St', Q', \mathcal{O}r', \mathcal{T}', \mu\mathcal{E}v'$.

**Proof sketch** By cases on the derivation of $E, St, Q, \mathcal{O}r, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p} {}_t E', St', Q', \mathcal{O}r', \mathcal{T}', \mu\mathcal{E}v'$, using Lemmas 15 and 16. $\square$

Moreover, if the rules that define $E, \sigma, M, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p} {}_t E', \sigma', M', \mathcal{T}', \mu\mathcal{E}v'$ (resp. $E, St, Q, \mathcal{O}r, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p} {}_t E', St', Q', \mathcal{O}r', \mathcal{T}', \mu\mathcal{E}v'$) require as assumption $E'', \sigma'', M'', \mathcal{T}'', \mu\mathcal{E}v'' \xrightarrow{p} {}_t \dots$ and the initial configuration is well-typed $\mathcal{E} \vdash E, \sigma, M : \mathcal{T}, \mathcal{T}, \mu\mathcal{E}v$ (resp. $\mathcal{E} \vdash E, St, Q, \mathcal{O}r, \mathcal{T}, \mu\mathcal{E}v$) then so is the initial configuration of the assumption, that is, there exists $\mathcal{T}''$ such that $\mathcal{E} \vdash E'', \sigma'', M'' : \mathcal{T}'', \mathcal{T}'', \mu\mathcal{E}v''$.

As an immediate consequence of Lemmas 17, 18, and 15 and the observation above, we obtain: if $Q_0$ satisfies Invariant 8, then in traces of $Q_0$, the tests $a \in T$ in rules (LetT) and (Let) and $\forall j \le m, a_j \in T_j$ in rule (Fun) always succeed. Moreover, in rules (NewT) and (New), we always have that $T$ is *fixed, bounded, or nonuniform*. In rules (IfT1), (IfT2), (If1), and (If2), the condition is in $\mathit{bool} = \{\mathit{false}, \mathit{true}\}$ (when it is a value, not an abort event value), so the condition $a \neq \mathit{true}$ is equivalent to $a = \mathit{false}$. In the rules for *find*, we have $r_k \in \{\mathit{false}, \mathit{true}\}$ when $r_k$ is a value (not an abort event value). In the rules (InsertT), (GetTE), (GetT1), (GetT2), (Insert), (GetE), (Get1), and (Get2), we have $a_j \in T_j$ for $j \le l$, where $\mathit{Tbl} : T_1 \times \dots \times T_l$. In the rules (EventT) and (Event), we have $a_j \in T_j$ for $j \le l$, where $e : T_1 \times \dots \times T_l$. In the rule (Return), we have $d \in T$. Finally, in the rule (OracleCall), the set $S$ of available oracles is equal to the one where we would not filter over the type of the oracle argument $b$.

## 2.5 Subset for the Initial Game

The variables are always defined with the current replication indices $\tilde{i}$, so we omit them, writing $x$ for $x[\tilde{i}]$; they are implicitly added by CryptoVerif. When a variable is used with the current replication indices at its definition, we can also omit the indices.

Along similar lines, the oracles $\mathcal{O}$ in oracle declarations are used without indices, and the current replication indices are implicitly added by CryptoVerif. The construct newOracle and the oracle calls cannot occur in games manipulated by CryptoVerif. They are used only inside proofs. The grammar of the resulting syntax is summarized in Figure 13.

We recommend using the constructs get and insert to manage key tables, instead of find or if with defined conditions. When no find nor if with defined conditions occurs in the game, by Invariant 2, all accesses to variable $x$ are of the form $x[\tilde{i}]$ where $\tilde{i}$ are the current replication