# CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels)

Bruno Blanchet

► To cite this version:

Bruno Blanchet. CryptoVerif: a Computationally-Sound Security Protocol Verifier (Initial Version with Communications on Channels). RR-9525, Inria Paris. 2023, pp.166. hal-04246199

HAL Id: hal-04246199

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

Submitted on 18 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
Inria

CryptoVerif: a
Computationally-Sound
Security Protocol Verifier

(Initial Version with
Communications on Channels)

Bruno Blanchet

RESEARCH
REPORT

Nº RR-9525

October 2023

Project-Team Prosecco

ISSN 0249-6399 ISRN INRIA/RR-RR-9525-FR+ENG
<figure><img src="image_2.png" /></figure>
<figure><img src="image_3.png" /></figure>

# CryptoVerif: a Computationally-Sound
Security Protocol Verifier
(Initial Version with Communications on Channels)

Bruno Blanchet*

Project-Team Prosecco

Research Report n° RR-9525 — October 2023 — 166 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 (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. 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

## (Version initiale avec communication sur des canaux)

**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. 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>15</td></tr><tr><td>2.3</td><td>Type System</td><td>17</td></tr><tr><td>2.4</td><td>Formal Semantics</td><td>21</td></tr><tr><td>2.4.1</td><td>Definition of the Semantics</td><td>21</td></tr><tr><td>2.4.2</td><td>Properties</td><td>30</td></tr><tr><td>2.4.3</td><td>Each Variable is Defined at Most Once</td><td>40</td></tr><tr><td>2.4.4</td><td>Variables are Defined Before Being Used</td><td>43</td></tr><tr><td>2.4.5</td><td>Typing</td><td>45</td></tr><tr><td>2.5</td><td>Subset for the Initial Game</td><td>46</td></tr><tr><td>2.6</td><td>Subsets used inside the Sequence of Games</td><td>48</td></tr><tr><td>2.7</td><td>Security Properties, Indistinguishability</td><td>50</td></tr><tr><td>2.7.1</td><td>Secrecy</td><td>58</td></tr><tr><td>2.7.2</td><td>Secrecy for a Bit</td><td>61</td></tr><tr><td>2.7.3</td><td>Correspondences</td><td>64</td></tr><tr><td>2.7.4</td><td>Computation of Advantages</td><td>70</td></tr><tr><td>2.7.5</td><td>Proof of Indistinguishability</td><td>79</td></tr><tr><td>2.7.6</td><td>Proof of query Equiv</td><td>81</td></tr><tr><td>2.8</td><td>Turing Machine Adversary</td><td>83</td></tr><tr><td>3</td><td>Collecting True Facts</td><td>86</td></tr><tr><td>3.1</td><td>User-defined Rewrite Rules</td><td>90</td></tr><tr><td>3.2</td><td>Collecting True Facts from a Game</td><td>91</td></tr><tr><td>3.3</td><td>Equational Prover</td><td>92</td></tr><tr><td>4</td><td>success: Criteria for Proving Security Properties</td><td>94</td></tr><tr><td>4.1</td><td>Secrecy</td><td>94</td></tr><tr><td>4.2</td><td>Correspondences</td><td>105</td></tr><tr><td>4.2.1</td><td>Example</td><td>105</td></tr><tr><td>4.2.2</td><td>Non-unique Events</td><td>108</td></tr><tr><td>4.2.3</td><td>Non-injective Correspondences</td><td>108</td></tr><tr><td>4.2.4</td><td>Injective Correspondences</td><td>113</td></tr><tr><td>5</td><td>Game Transformations</td><td>120</td></tr><tr><td>5.1</td><td>Syntactic Game Transformations</td><td>120</td></tr><tr><td>5.1.1</td><td>auto SArename</td><td>120</td></tr><tr><td>5.1.2</td><td>expand tables</td><td>121</td></tr><tr><td>5.1.3</td><td>expand</td><td>121</td></tr><tr><td>5.1.4</td><td>prove unique</td><td>122</td></tr><tr><td>5.1.5</td><td>remove assign</td><td>122</td></tr><tr><td>5.1.6</td><td>use variable</td><td>123</td></tr><tr><td>5.1.7</td><td>SArename</td><td>124</td></tr><tr><td>5.1.8</td><td>move</td><td>125</td></tr><tr><td>5.1.9</td><td>move array</td><td>126</td></tr><tr><td>5.1.10</td><td>move up</td><td>126</td></tr></table>
<table><tbody><tr><td>5.1.11</td><td>move_if Fun</td><td>128</td></tr><tr><td>5.1.12</td><td>insert_event</td><td>129</td></tr><tr><td>5.1.13</td><td>insert</td><td>129</td></tr><tr><td>5.1.14</td><td>replace</td><td>129</td></tr><tr><td>5.1.15</td><td>merge</td><td>130</td></tr><tr><td>5.1.16</td><td>merge arrays</td><td>131</td></tr><tr><td>5.1.17</td><td>guess i</td><td>132</td></tr><tr><td>5.1.18</td><td>guess x[c<sub>1</sub>,...,c<sub>m</sub>]</td><td>140</td></tr><tr><td>5.1.19</td><td>guess branch</td><td>143</td></tr><tr><td>5.1.20</td><td>global depAnal</td><td>146</td></tr><tr><td>5.1.21</td><td>simplify</td><td>147</td></tr><tr><td>5.1.22</td><td>all simplify</td><td>151</td></tr><tr><td>5.1.23</td><td>success simplify</td><td>151</td></tr><tr><td>5.2</td><td>crypto: Applying the Security Assumptions on Primitives</td><td>159</td></tr><tr><td>6</td><td>Proof Strategy</td><td>159</td></tr><tr><td>7</td><td>Conclusion</td><td>159</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 [20, 61, 62]: 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. This calculus is inspired by the pi-calculus and by the calculi of [54] and of [50]. 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 mentioned above, 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 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 input the arguments of the oracle and send its result back. 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.

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 [1], 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., [5,33,37,38,46] and the survey [36]). 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 [35] was developed based on [37] 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 [7,8] 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 [65,66]. Canetti [30] introduced the notion of universal composability. With Herzog [32], 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 [22] for verifying protocols in this framework. Process calculi have been designed for representing cryptographic games, such as the probabilistic polynomial-time calculus of [54] and the cryptographic lambda-calculus of [57]. Logics have also been designed for proving security protocols in the computational model, such as the computational variant of PCL (Protocol Composition Logic) [42,43] and CIL (Computational Indistinguishability Logic) [11]. Canetti et al. [31] 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 model.
sense, but except for [32] 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 [41,50,52,64] provide computational security guarantees. For instance, [50] 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 [6]. The recent tool OWL [44] 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 [58]. 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 [39, 40].

The tool CertiCrypt [12, 13, 15, 17, 18] enables the machine-checked construction and verification of cryptographic proofs by sequences of games [20,63]. It relies on the general-purpose proof assistant Coq, which is widely believed to be correct. Nowak et al. [3, 55, 56] follow a similar idea by providing Coq proofs for several cryptographic primitives. More recently, frameworks for cryptographic proofs in Coq, FCF [59], and in Isabelle, CryptHOL [16], have been designed and used for proving cryptographic schemes. EasyCrypt [14], 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 [10], e-voting [34], AWS key management [4], and distance bounding [27]. 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 [9] 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 [24] to help cryptographers, not only for the verification, but also by generating the proofs by sequences of games [20,63], 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 [48,49] which was limited either to passive adversaries or to a single session of the protocol. More recently, Tšahhirov and Laud [51, 67] 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$.

# 2 A Calculus for Cryptographic Games

## 2.1 Syntax and Informal Semantics

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

It also uses types, denoted by $T$, which are non-empty, countable sets of values. We assume that there exists an efficient injection from each type to the set of bitstrings, and that its inverse is also efficiently computable. 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 = \{\text{true, false}\}$, where false is 0 and true is 1; bitstring is the set of all bitstrings; $bitstring_{\perp} = bitstring \cup \{\perp\}$ where $\perp$ is a special symbol; $[1, n]$ is the set of integers $\{1, \dots, n\}$, where $n$ is a parameter. (We consider integers as bitstrings without leading zeroes.)

The calculus also uses function symbols $f$. Each function symbol comes with a type declaration $f: T_1 \times \dots \times T_m \rightarrow 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 calculus, terms represent computations on bitstrings. The replication index $i$ is an integer which serves in distinguishing different copies of a replicated process $!^{i \le n}$. (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 output processes and explained below. These constructs conclude by evaluating a term, instead of executing a process. The construct `event_abort e` executes event $e$ (without argument) and aborts the game.

The calculus distinguishes two kinds of processes: input processes $Q$ are ready to receive a message on a channel; output processes $P$ output a message on a channel after executing some internal computations. The input process $0$ does nothing; $Q \mid Q'$ is the parallel composition of $Q$ and $Q'$; $!^{i \le n} Q$ represents $n$ copies of $Q$ in parallel, each with a different value of $i \in [1, n]$;
<figure><img src="image_4.png" /><figcaption>Figure 1: Syntax of the process calculus</figcaption></figure>
newChannel c; Q creates a new private channel c and executes Q; this construct is useful in proofs, but does not occur in games manipulated by CryptoVerif. The semantics of the input c[M₁, ..., Mₜ](p); P will be explained below together with the semantics of the output.

The output process new x[i] : T; P chooses a new random value in T, stores it in x[i], and executes P. The abbreviation ̃i stands for a sequence of replication indices i₁, ..., iₘ. 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₁ and D₂ 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 ∈ [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, \text{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' + 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 new x[i] : T; P. Function symbols represent deterministic functions, so all random numbers must be chosen by new x[i] : T. Deterministic functions make automatic syntactic manipulations easier: we can duplicate a term without changing its value.
The process let $x[\tilde{i}] : T = M$ in $P$ stores the value of $M$ (which must be in $T$) in $x[\tilde{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.

The process *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 process. Events are used in particular for specifying security properties.

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

Next, we explain the process 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_{jl_j}$) $\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$ such that 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$ such that 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}$ such that defined($M_{j1}, \dots, M_{jl_j}$) $\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_{jl_j}$ 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_{jl_j}$) $\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 \frac{\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 $\text{defined}(M_1, \dots, M_l) \wedge 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 $\text{defined}(M_1, \dots, M_l) \wedge M$ then $P$ else $P'$. The conjunct $M$ can be omitted when it is true, writing if $\text{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* $\text{Tbl}(M_1, \dots, M_l); P$ inserts the element $M_1, \dots, M_l$ in the table $\text{Tbl}$; *get* $\text{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 $\text{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_{\text{get}}(S)$ where $S$ is the set of indices of suitable elements, with $d(D_{\text{get}}(S), \text{uniform}) \le \epsilon_{\text{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 [*unique?*] stands for either [*unique*<sub>e</sub>] or empty. The empty case has just been explained. When the *get* is marked [*unique*<sub>e</sub>] 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 [*unique?*] is empty. CryptoVerif internally translates the *insert* and *get* constructs into *find*.

Let us explain the output $\overline{c[M_1, \dots, M_l](N)}; Q$. A channel $c[M_1, \dots, M_l]$ consists of both a channel name $c$ and a tuple of terms $M_1, \dots, M_l$. Channel names $c$ can be declared private by newChannel $c$; the adversary can never have access to channel $c[M_1, \dots, M_l]$ when $c$ is private. (This is useful in the proofs, although all channels of protocols are often public.) Terms $M_1, \dots, M_l$ are intuitively analogous to IP addresses and ports, which are numbers that the adversary may guess. A semantic configuration always consists of a single output process (the process currently being executed) and several input processes. When the output process executes $c[M_1, \dots, M_l](N); Q$, one looks for an input on channel $c[M'_1, \dots, M'_l]$, where $M'_1, \dots, M'_l$ evaluate to the same bitstrings as $M_1, \dots, M_l$, in the available input processes. If no such input process is found, the process blocks. Otherwise, one such input process $c[M'_1, \dots, M'_l](x[\tilde{i}] : T)$; $P$ is chosen randomly according to the probability distribution $D_{\text{in}}(S)$ where $S$ is the multiset of suitable input processes. The communication is then executed: the output message $N$ is evaluated and stored in $x[\tilde{i}]$ if it is in $T$ (otherwise the process blocks). Finally, the output process $P$ that follows the input is executed. The input process $Q$ that follows the output is stored in the available input processes for future execution. The input construct can be generalized to patterns instead of variables similarly to the *let* case; when pattern-matching fails, the input process executes *yield*. The syntax requires an output to be followed by an input process, as in [50]. If one needs to output several messages consecutively, one can simply insert fictitious inputs between the
outputs. The adversary can then schedule the outputs by sending messages to these inputs.

Using different channels for each input and output allows the adversary to control the network. For instance, we may write $!^{i \le n} c[i](x[i] : T) ... c'[i] \langle M \rangle ...$ The adversary can then decide which copy of the replicated process receives its message, simply by sending it on $c[i]$ for the appropriate value of $i$.

The *yield* construct is an abbreviation for $\overline{yield}(\langle \rangle)$. By performing an output, this construct returns control to the adversary, which is going to receive the message. 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*, *new*, or *insert* and in *yield* may be omitted after *let*. A trailing 0 after an output may be omitted.

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 $!^{i \le n} Q$ binds the replication index $i$ in $Q$. The find construct find[unique?] ($\bigoplus_{j=1}^m u_{j1}[i] = i_{j1} \le n_{j1}, \dots, u_{jm_j}[i] = i_{jm_j} \le n_{jm_j}$ such that defined($M_{j1}, \dots, M_{j_{l_j}}$) $\land$ $M_j$ then ...) else ... binds the replication indices $i_{j1}, \dots, i_{jm_j}$ in defined($M_{j1}, \dots, M_{j_{l_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 $!^{i_1 \le n_1} \dots !^{i_m \le n_m} \text{let } x[i_1, \dots, i_m] : T = M \text{ in } \dots$ More formally, we require the following invariant:

**Invariant 1 (Single definition)** The process $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), 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.

In get[unique?] Tbl($p_1, \dots, p_l$) such that $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[i]$ can be new $x[i] : T$, a let, get, or input that contains the pattern $x[i] : T$, or find... $x[i] = i \le n$...

**Invariant 2 (Defined variables)** The process $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 process or term;

* or in $M'_j$ in a process or term of the form find ($\bigoplus_{j=1}^{m''} \tilde{u}_j[i] = \tilde{i}_j \le \tilde{n}_j$ such that 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$ such that defined($M'_{j1}$, ..., $M'_{jl_j}$) ∧ $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 new $x[\tilde{i}] : T; P$;

* inside $N$ in new $x[\tilde{i}] : 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_{j_l}$) ∧ $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_{j_l}$) ∧ $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 $c[M_1, \dots, M_l](p); P$ when $x[\tilde{i}] : T$ is bound in the pattern $p$.

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.

**Invariant 3 (Variables defined in find and get conditions)** The process $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 process $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 input channels and defined conditions)** The process $Q_0$ satisfies Invariant 5 if and only if all terms in input channels $c[M_1, ..., M_l]$ and in conditions defined($M_1$, ..., $M_l$) in find are simple.

Terms that are not simple are handled by expanding them into their corresponding processes. Invariant 5 is needed because terms in input channels cannot be expanded, as we need an output process to put the computations coming from expanded terms, and similarly 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, ..., M_m]$ are simple.

The last 3 invariants did not appear in previous versions of the calculus because all terms were simple.

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

* Shoup events occur only in processes of the form `event_abort e` in $Q_0$,

* non-unique events occur only in `find[unique_e]` or `get[unique_e]` in $Q_0$, and

* other events occur in `event e(M_1, ..., M_l)` or in `event_abort e` in $Q_0$.

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

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 `fc(P)` the set of free channels of $P$. (We use similar notations for input processes.)

## 2.2 Example

Let us introduce two cryptographic primitives that we use below.

**Definition 2** Let $T_{mk}$ and $T_{ms}$ be types that correspond intuitively to keys and message authentication codes, respectively; $T_{mk}$ is a fixed-length type. A message authentication code scheme MAC [19] consists of two function symbols:

* `mac`: `bitstring` $\times$ $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` $\times$ $T_{mk}$ $\times$ $T_{ms} \to \text{bool}$ is a verification algorithm such that $\text{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, $\text{verify}(m, k, t)$ is typically `mac(m, k) = t`.)

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

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

$$ \text{Succ}_{\text{MAC}}^{\text{uf-cma}}(t, q_m, q_v, l) = \max_{\mathcal{A}} \Pr \left[ k \stackrel{R}{\leftarrow} T_{mk}; (m, s) \leftarrow \mathcal{A}^{\text{mac}(.,k), \text{verify}(.,k,..)} : \text{verify}(m, k, s) \wedge \text{m was never queried to the oracle mac(., k)} \right] $$
where the adversary $\mathcal{A}$ is any probabilistic Turing machine that runs in time at most $t$, calls $\text{mac}(., k)$ at most $q_m$ times with messages of length at most $l$, and calls $\text{verify}(., k, .)$ at most $q_v$ times with messages of length at most $l$.

$\text{Succ}_{\text{MAC}}^{\text{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 $\text{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 [23, 24], the length of keys is determined by a security parameter $\eta$, and a MAC is UF-CMA when $\text{Succ}_{\text{MAC}}^{\text{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_0$, $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 $\text{Succ}_{\text{MAC}}^{\text{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 $\text{Succ}_{\text{MAC}}^{\text{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 $\text{SE}$ [19] consists of two function symbols:

* $\text{enc} : \text{bitstring} \times 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,

* $\text{dec} : T_e \times T_k \to \text{bitstring}_\perp$ is the decryption algorithm taking as arguments the cleartext 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 $\text{LR}(x, y, b) = x$ if $b = 0$ and $\text{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{\mathcal{A}}{\leftarrow} r \stackrel{R}{\leftarrow} T_r; \text{enc}(\text{LR}(., ., 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}(\text{LR}(., ., 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}(\text{LR}(., ., b), k, r)$ returns $r \stackrel{R}{\leftarrow} T_r$; $\text{enc}(\text{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 [19]. 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 process $Q_0$:

$$\begin{align*}
Q_0 &= \text{start}(); \quad \text{new } x_k : T_l; \quad \text{new } x_{mk} : T_{mk}; \overline{c}\langle\rangle; (Q_A | Q_B) \\
Q_A &= !^{i \le n} c_A[i](); \quad \text{new } x'_k : T_k; \quad \text{new } x_r : T_r; \\
\text{let } x_m : \text{bitstring} &= \text{enc}(\text{k2b}(x'_k), x_k, x_r) \text{ in } \overline{c_A[i]}\langle x_m, \text{mac}(x_m, x_{mk}) \rangle \\
Q_B &= !^{i' \le n} c_B[i'](x'_m, x_{ma}); \quad \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 } \overline{c_B[i']}\langle\rangle
\end{align*}$$

When $Q_0$ receives a message on channel start, it begins execution: it generates the keys $x_k$ and $x_{mk}$ randomly. Then it yields control to the adversary, by outputting on channel c. After this output, n copies of processes for A and B are ready to be executed, when the adversary outputs on channels $c_A[i]$ or $c_B[i]$ respectively. In a session that runs as expected, the adversary first sends a message on $c_A[i]$. Then $Q_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 sends the ciphertext and the MAC on $c_A[i]$. 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 message on $c_B[i]$. When $Q_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 send messages 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 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), the type-checking algorithm proceeds in two passes. In the first pass, it 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$. (For instance, the definition of $x[i_1, \dots, i_m]$ occurs under $!^{i_1 \le n_1}, \dots, !^{i_m \le n_m}$ 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 new $x[\tilde{i}] : T$ or in a pattern $x[\tilde{i}] : T$ in an assignment, an input, or a get. In the find construct, find...$x[\tilde{i}] = i \le n$, the type T of x is $T = [1, n]$. 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.

In the second pass, the process is typechecked in the type environment $\mathcal{E}$ using the rules of Figures 2 and 3. 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$ and $\mathcal{E} \vdash Q$ mean that the output process $P$ and the input process $Q$ are well-typed in environment $\mathcal{E}$, respectively.

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 new $x[\tilde{i}] : 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 new $x[\tilde{i}] : 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

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} \text{ suchthat} \\
\text{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$ can have any type (because it aborts the game); the event $e$ must be declared without argument, which we denote by $e:()$.

The type system for processes requires each subterm to be well-typed. In $!^{i \le n} Q$, $i$ is of type $[1, n]$ in $Q$. The processes new, let, if, find, insert, get, event, and event_abort are typed similarly to the corresponding terms.

We say that an occurrence of a term $M$ in a process $Q$ is of type $T$ when $\mathcal{E} \vdash M : T$ where $\mathcal{E}$ is the type environment of $Q$ extended with $i \mapsto [1, n]$ for each replication $!^{i \le n}$ above $M$
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 \rightarrow 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 \rightarrow 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 \text{ new } x[\tilde{i}] : 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) $$

$$ \begin{array}{l} \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 \end{array} $$

$$ \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} \\ \text{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 : T'} \qquad (TEventAbortT) $$

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 \rightarrow 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 input processes:

$$ \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 !^{i \le n} Q} \qquad (\text{TRepl}) $$

$$ \frac{\mathcal{E} \vdash Q}{\mathcal{E} \vdash \text{newChannel } c; Q} \qquad (\text{TNewChannel}) $$

$$ \frac{\forall j \le l, \mathcal{E} \vdash M_j : T'_j \qquad \mathcal{E} \vdash p : T \qquad \mathcal{E} \vdash P}{\mathcal{E} \vdash c[M_1, \dots, M_l](p); P} \qquad (\text{TIn}) $$

Typing rules for output processes:

$$ \frac{\forall j \le l, \mathcal{E} \vdash M_j : T'_j \qquad \mathcal{E} \vdash N : T \qquad \mathcal{E} \vdash Q}{\mathcal{E} \vdash \overline{c[M_1, \dots, M_l]} \langle N \rangle; Q} \qquad (\text{TOut}) $$

$$ \frac{T \text{ fixed, bounded, or nonuniform} \qquad \mathcal{E} \vdash x[\tilde{i}] : T \qquad \mathcal{E} \vdash P}{\mathcal{E} \vdash \text{new } x[\tilde{i}] : T; P} \qquad (\text{TNew}) $$

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

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

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

$$ \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} \qquad (\text{TFind}) $$

$$ \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} \qquad (\text{TFind}) $$

$$ \forall j \le m, \mathcal{E} \vdash P_j \qquad \mathcal{E} \vdash P \qquad (\text{TFind}) $$

$$ \mathcal{E} \vdash \text{find}[\text{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{ such that } \right. \\ \left. \text{defined}(M_{j1}, \dots, M_{jl_j}) \wedge M_j \text{ then } P_j \right) \text{ else } P \qquad (\text{TFind}) $$

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

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

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

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

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

<caption>Figure 3: Typing rules (2)</caption>
in $Q$ and with $i_{j1} \mapsto [1, n_{j1}], \dots, i_{jm_j} \mapsto [1, n_{jm_j}]$ for each 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_{jl_j}$) $\land$ $M_j$ then $P_j$) else $P$ such that the considered occurrence of $M$ is in the condition defined($M_{j1}, \dots, M_{jl_j}$) $\land$ $M_j$.

**Invariant 7 (Typing)** The process $Q_0$ satisfies Invariant 7 if and only if the type environment $\mathcal{E}$ for $Q_0$ is well-defined, and $\mathcal{E} \vdash Q_0$.

We require the adversary to be well-typed. This requirement does not restrict its computing 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.

## 2.4 Formal Semantics

### 2.4.1 Definition of the Semantics

The formal semantics of our calculus is presented in Figures 4, 5, 7, 8, and 9.

In this semantics, each term $M$ or process $P$ or $Q$ is labeled by a program point $\mu$, replacing $M$ with $^\mu 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 process. These program points are simply constant tags, and the initial process is tagged with a distinct program point at each subterm and subprocess.

A semantic configuration is a sextuple $E, (\sigma, P), Q, Ch, T, \mu\mathcal{E}v$, where

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

* $(\sigma, P)$ is the output process $P$ currently scheduled, with the associated mapping sequence $\sigma$ which gives values of replication indices.

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 Dom($\sigma$) = $[i_1, \dots, i_m]$ to be the sequence of current replication indices and 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]$.

* $Q$ is the multiset of input processes running in parallel with $P$, with their associated mapping sequences giving values of replication indices.

* $Ch$ is the set of channels already created.

* $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\mathcal{E}v$ 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) \mid (\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 `event_abort` ($\mu, \tilde{\alpha}$) : $e$, and the processes $P$ can be `abort`, corresponding to the situation in which the game has been aborted. These additional terms and processes are not tagged with program points. (They do not occur in the initial process.)

The semantics is defined by reduction rules of the form $E, (\sigma, P), Q, Ch, T, \mu\mathcal{E}v \xrightarrow{p} t E', (\sigma', P'), Q', Ch', T', \mu\mathcal{E}v'$ meaning that $E, (\sigma, P), Q, Ch, T, \mu\mathcal{E}v$ reduces to $E', (\sigma', P'), Q', Ch', 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, (\sigma, P), Q, Ch, T, \mu\mathcal{E}v \to E', (\sigma', P'), Q', Ch', T', \mu\mathcal{E}v'] = \sum_{E, (\sigma, P), Q, Ch, T, \mu\mathcal{E}v \xrightarrow{p} t E', (\sigma', P'), Q', Ch', T', \mu\mathcal{E}v'} p $$

The probability of a trace $Tr = E_1, (\sigma_1, P_1), Q_1, Ch_1, T_1, \mu\mathcal{E}v_1 \xrightarrow{p_1} t_1 \dots \xrightarrow{p_{m-1}} t_{m-1} E_m, (\sigma_m, P_m), Q_m, Ch_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 4 and 5, 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 (ReplIndex) 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 `event_abort` $e$ or a find[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_{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 [unique$_e$], and we choose an element $v_0 = (j', a'_1, \dots, a'_{m'_j})$ of $S$ randomly according to the distribution $D_{find}(S)$, store the corresponding indices $a'_1, \dots, a'_{m'_j}$ in $u_{j'_1}[\sigma(\tilde{i})], \dots, u_{j'_m}[\sigma(\tilde{i})]$ by extending the environment accordingly, and we continue with the selected branch $N'_j$. If the find is marked [unique$_e$] and $S$ has a single element, we do the same. If the find is marked [unique$_e$] and $S$ has several elements, we execute the event $e$ (Rule (FindT3)). We recall that $D_{find}(S)(v_0)$ denotes the probability of choosing $v_0$ in the distribution $D_{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 insert nor event (Invariant 4), the table contents and the sequence of events are left unchanged by the evaluation of the condition of find.
$$E, \sigma, \mu^i, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{1} E, \sigma, \sigma(i), \mathcal{T}, \mu\mathcal{E}v \qquad (\text{ReplIndex})$$

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

$$E, \sigma, \mu^x[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} \qquad (\text{Fun})$$

$$\frac{a \in T \quad E' = E[x[\sigma(\tilde{i})] \mapsto a]}{} \qquad (\text{NewT})$$

$$E, \sigma, \mu^{\text{new}} x[\tilde{i}] : T; N, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{D_{\mathcal{T}}(a)}_{N(a)} E', \sigma, N, \mathcal{T}, \mu\mathcal{E}v$$

$$\frac{a \in T \quad E' = E[x[\sigma(\tilde{i})] \mapsto a]}{} \qquad (\text{LetT})$$

$$E, \sigma, \mu^{\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$$

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

$$\frac{a \neq \text{true}}{} \qquad (\text{IfT2})$$

$$E, \sigma, \mu^{\text{if}} \text{ a then } N \text{ else } N', \mathcal{T}, \mu\mathcal{E}v \xrightarrow{1} E, \sigma, N', \mathcal{T}, \mu\mathcal{E}v$$

$(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^{\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 \qquad (\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', 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^{\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 \qquad (\text{FindT1})$$

$$\text{First four lines as in (FindT1)} \qquad S = \{v_k \mid 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 } 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$$

$$\text{First four lines as in (FindT1)} \qquad S = \{v_k \mid 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 } 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 \qquad (\text{FindT3})$$

<caption>Figure 4: 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}_{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 5: 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] \\
      & \mu f(a_1, \dots, a_{k-1}, [], M_{k+1}, \dots, M_m) \\
      & \mu \text{let } x[\tilde{i}] : T = [] \text{ in } N \\
      & \mu \text{if } [] \text{ then } N \text{ else } N' \\
      & \mu \text{event } e(a_1, \dots, a_{k-1}, [], M_{k+1}, \dots, M_l); N \\
      & \mu \text{insert } Tbl(a_1, \dots, a_{k-1}, [], M_{k+1}, \dots, M_l); N
\end{align*}
$$

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

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 6. 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 value $a$ or an abort event value `event_abort` $(\mu, \tilde{a}) : e$. We have $E, \sigma, M, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{1}^* E, \sigma, M, \mathcal{T}, \mu\mathcal{E}v$ and, if $E, \sigma, M, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p}^{} E', \sigma', M', \mathcal{T}', \mu\mathcal{E}v'$ and $E', \sigma', M', \mathcal{T}', \mu\mathcal{E}v' \xrightarrow{p'}^{} E'', \sigma'', M'', \mathcal{T}'', \mu\mathcal{E}v''$,
$E, \{(\sigma, \mu 0)\} \uplus Q, Ch \rightsquigarrow E, Q, Ch$ (Nil)

$E, \{(\sigma, \mu(Q_1 | Q_2))\} \uplus Q, Ch \rightsquigarrow E, \{(\sigma, Q_1), (\sigma, Q_2)\} \uplus Q, Ch$ (Par)

$E, \{(\sigma, \mu!^{i \le n} Q)\} \uplus Q, Ch \rightsquigarrow E, \{(\sigma[i \mapsto a], Q) | a \in [1, n]\} \uplus Q, Ch$ (Repl)

$\frac{c' \notin Ch}{E, \{(\sigma, \mu \text{newChannel } c; Q)\} \uplus Q, Ch \rightsquigarrow E, \{(\sigma, Q\{c'/c\})\} \uplus Q, Ch \cup \{c'\}}$ (NewChannel)

$\frac{E, \sigma, M_j, \emptyset, \emptyset \xrightarrow{1} E, \sigma, M'_j, \emptyset, \emptyset}{E, \{(\sigma, C[M_j])\} \uplus Q, Ch \rightsquigarrow E, \{(\sigma, C[M'_j])\} \uplus Q, Ch}$ (Input)

where $C = \mu c[a_1, \dots, a_{j-1}, [], M_{j+1}, \dots, M_l](x[i] : T); P$
reduce$(E, Q, Ch)$ is the normal form of $E, Q, Ch$ by $\rightsquigarrow$

<caption>Figure 7: Semantics (3): input processes</caption>

then $E, \sigma, M, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p \times p'} \mathcal{T}_{t,t'} E'', \sigma'', M'', \mathcal{T}'', \mu\mathcal{E}v''$: 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 7 defines the semantics of input processes. We use an auxiliary reduction relation $\rightsquigarrow$, for reducing input processes. This relation transforms configurations of the form $E, Q, Ch$. Rule (Nil) removes nil processes. Rules (Par) and (Repl) expand parallel compositions and replications, respectively. Rule (NewChannel) creates a new channel and adds it to $Ch$. Semantic configurations are considered equivalent modulo renaming of channels in $Ch$, so that a single semantic configuration is obtained after applying (NewChannel). Rule (Input) evaluates the terms in the input channel. The input itself is not executed: the communication is done by the (Output) rule. In the (Input) rule, the terms $M_1, \dots, M_l$ are simple by Invariant 5, so their evaluation is deterministic (the unique result is obtained with probability 1), the environment $E$, the contents of tables $\mathcal{T}$, and the sequence of events $\mu\mathcal{E}v$ are unchanged, and $\mathcal{T}$ and $\mu\mathcal{E}v$ are unused, that is why we can write $E, \sigma, M_j, \emptyset, \emptyset \xrightarrow{1} E, \sigma, M'_j, \emptyset, \emptyset$ using empty $\mathcal{T}$ and $\mu\mathcal{E}v$, written $\emptyset$. The relation $\rightsquigarrow$ is convergent (confluent and terminating), so it has normal forms. Processes in $Q$ in configurations $E, (\sigma, P), Q, Ch, \mathcal{T}, \mu\mathcal{E}v$ are always in normal form by $\rightsquigarrow$, so they always start with an input.

Finally, Figures 8 and 9 define the semantics of output processes. Most of these rules are very similar to those for terms: they just use processes 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 process `abort`. Similarly to the case of terms, Rules (Ctx) and (CtxEvent) allow evaluating terms under a context inside a process. In these rules, $C$ is an elementary context, of one of the forms defined in Figure 10.

Rule (Output) performs communications: it selects an input on the desired channel randomly, and immediately executes the communication. (The process blocks if no suitable input is available.) The scheduled process after this rule is the receiving process. The input processes that follow the output are stored in the available input processes, after reducing them by rules of Figure 7. In this rule, $S$ is a multiset. When we take probabilities over multisets, we consider that $D_{\text{in}}(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_{\text{in}}(S)$, so that the probability of choosing any element equal to $(\sigma', Q_0)$ is in fact $S(\sigma', Q_0) \times D_{\text{in}}(S)(\sigma', Q_0)$.

After finishing execution of a process, the system produces the sequence of executed events
Same assumption as in (FindTE) $r_{k_0} = \text{event_abort}(\mu', \tilde{a}) : e$

(FindE)

$$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), Q, Ch, T, \mu \mathcal{E}v$$

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

First four lines as in (FindT1)

$$S = \{v_k | r_k = \text{true}\}$$

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

$$v_0 = (j', a'_1, \dots, a'_{m'_{j'}}) \in S$$

$$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 \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), Q, Ch, 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, P_j'), Q, Ch, T, \mu \mathcal{E}v$$

(Find1)

First four lines as in (FindT1)

$$S = \{v_k | r_k = \text{true}\} = \emptyset$$

(Find2)

$$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), Q, Ch, T, \mu \mathcal{E}v$$

$$\xrightarrow{p_1 \dots p_l}^{D_j \wedge M_j \text{ then } P_j} E, (\sigma, P), Q, Ch, T, \mu \mathcal{E}v$$

First four lines as in (FindT1)

$$S = \{v_k | r_k = \text{true}\}$$

$$|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), Q, Ch, T, \mu \mathcal{E}v$$

$$\xrightarrow{p_1 \dots p_l}^{D_{GE}(k_0)}_{t_1 \dots t_l F_3} E, (\sigma, \text{abort}), Q, Ch, T, (\mu \mathcal{E}v, (\mu, \text{Im}(\sigma)) : e)$$

(Find3)

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

(Insert)

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'), Q, Ch, T, \mu \mathcal{E}v$$

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

(GetE)

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

$$k_0 \in S \qquad \text{Tbl}(a_1, \dots, a_l) = v_{k_0}$$

$$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'), Q, Ch, T, \mu \mathcal{E}v$$

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

(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'), Q, Ch, T, \mu \mathcal{E}v$$

$$\xrightarrow{p_1 \dots p_m}^{D_{G2}(k_0)}_{t_1 \dots t_m G_2} E, (\sigma, P'), Q, Ch, T, \mu \mathcal{E}v$$

(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'), Q, Ch, T, \mu \mathcal{E}v$$

$$\xrightarrow{p_1 \dots p_m}^{D_{G3}(k_0)}_{t_1 \dots t_m G_3} E, (\sigma, \text{abort}), Q, Ch, T, (\mu \mathcal{E}v, (\mu, \text{Im}(\sigma)) : e)$$

(Get3)

<caption>Figure 8: Semantics (4): output processes, first part</caption>
$$ \frac{a \in T \quad E' = E[x[\sigma(\tilde{i})] \mapsto a]}{E, (\sigma, \mu \text{new } x[\tilde{i}] : T; P), Q, Ch, T, \mu \mathcal{E}v \xrightarrow{D_T(a)}_{N(a)} E', (\sigma, P), Q, Ch, T, \mu \mathcal{E}v} \qquad (\text{New}) $$

$$ \frac{a \in T \quad E' = E[x[\sigma(\tilde{i})] \mapsto a]}{E, (\sigma, \mu \text{let } x[\tilde{i}] : T = a \text{ in } P), Q, Ch, T, \mu \mathcal{E}v \xrightarrow{1} E', (\sigma, P), Q, Ch, T, \mu \mathcal{E}v} \qquad (\text{Let}) $$

$$ E, (\sigma, \mu \text{if true then } P \text{ else } P'), Q, Ch, T, \mu \mathcal{E}v \xrightarrow{1} E, (\sigma, P), Q, Ch, T, \mu \mathcal{E}v \qquad (\text{If1}) $$

$$ \frac{a \neq true}{E, (\sigma, \mu \text{if } a \text{ then } P \text{ else } P'), Q, Ch, T, \mu \mathcal{E}v \xrightarrow{1} E, (\sigma, P'), Q, Ch, T, \mu \mathcal{E}v} \qquad (\text{If2}) $$

$$ \frac{E, (\sigma, \mu \text{event } e(a_1, \dots, a_l); P), Q, Ch, T, \mu \mathcal{E}v \xrightarrow{1}}{E, (\sigma, P), Q, Ch, T, (\mu \mathcal{E}v, (\mu, \text{Im}(\sigma)) : e(a_1, \dots, a_l))} \qquad (\text{Event}) $$

$$ \frac{E, (\sigma, \mu \text{event\_abort } e), Q, Ch, T, \mu \mathcal{E}v \xrightarrow{1} E, (\sigma, \text{abort}), Q, Ch, T, (\mu \mathcal{E}v, (\mu, \text{Im}(\sigma)) : e)}{(\text{EventAbort})} $$

$$ \frac{E, \sigma, N, T, \mu \mathcal{E}v \xrightarrow{p} t E', \sigma', N', T', \mu \mathcal{E}v'}{E, (\sigma, C[N]), Q, Ch, T, \mu \mathcal{E}v \xrightarrow{p} t E', (\sigma', C[N'])), Q, Ch, T', \mu \mathcal{E}v'} \qquad (\text{Ctx}) $$

$$ E, (\sigma, C[\text{event\_abort } (\mu, \tilde{a}) : e]), Q, Ch, T, \mu \mathcal{E}v \xrightarrow{1} E, (\sigma, \text{abort}), Q, Ch, T, (\mu \mathcal{E}v, (\mu, \tilde{a}) : e) \qquad (\text{CtxEvent}) $$

$$ \frac{E, Q', Ch' = \text{reduce}(E, \{(\sigma, Q'')\}, Ch)}{S = \{(\sigma', Q) \in Q | Q = \mu''c[a_1, \dots, a_l][x[\tilde{i}] : T'. P' \text{ and } b \in T' \text{ for some } \mu'', \sigma', x', T', P'\} (\sigma', Q_0) \in S \quad Q_0 = \mu'c[a_1, \dots, a_l][x[\tilde{i}] : T]. P} $$

$$ \frac{E, (\sigma, \mu \overline{c}[a_1, \dots, a_l] \langle b \rangle.Q''), Q, Ch, T, \mu \mathcal{E}v \xrightarrow{S(\sigma', Q_0) \times D_{\text{in}}(S)(\sigma', Q_0)}_{O(\sigma', Q_0)} E[x[\sigma'(\tilde{i})] \mapsto b], (\sigma', P), Q \uplus Q' \setminus \{(\sigma', Q_0)\}, Ch', T, \mu \mathcal{E}v}{(\text{Output})} $$

<caption>Figure 9: Semantics (5): output processes, second part</caption>

### $\mathcal{E}v$. 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 process $Q$ is initConfig($Q$) = $\emptyset$, $(\sigma_0, \mu \text{start}\langle\rangle)$, $Q, Ch, \emptyset, \emptyset$ where $\emptyset, Q, Ch = \text{reduce}(\emptyset, \{(\sigma_0, Q)\}, \text{fc}(Q))$ and $\sigma_0$ is the empty mapping sequence.

A trace of $Q$ is a trace that starts from initConfig($Q$): $\text{Tr} = \text{initConfig}(Q) \xrightarrow{p_1} t_1 \dots \xrightarrow{p_{m-1}} t_{m-1}$
$\text{Conf}_m$. Let $\mathcal{T}$ be the set of all traces of $Q$.

Let $\mathcal{T}_{\text{full}}$ be the set of full traces of $Q$, that is, the set of traces of $\mathcal{T}$ whose last configuration
$$
\begin{align*}
C ::= & \mu \text{let } x[\tilde{i}] : T = [] \text{ in } P \\
      & \mu \text{if } [] \text{ then } P \text{ else } P' \\
      & \overline{\mu c[a_1, \dots, a_{k-1}, [], M_{k+1}, \dots, M_l] \langle N \rangle . Q} \\
      & \overline{\mu c[a_1, \dots, a_l] \langle [] \rangle . Q} \\
      & \mu \text{insert } Tbl(a_1, \dots, a_{k-1}, [], M_{k+1}, \dots, M_l); P \\
      & \mu \text{event } e(a_1, \dots, a_{k-1}, [], M_{k+1}, \dots, M_l); P
\end{align*}
$$

<caption>Figure 10: Process contexts</caption>

$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) \xrightarrow{p_1} t_1 \dots \xrightarrow{p_{m-1}} t_{m-1} Conf_m$, recall that $\text{Pr}[Tr] = p_1 \times \dots \times p_{m-1}$. We define

$$
\begin{align*}
\Pr[Q : \varphi] &= \sum_{Tr \in \mathcal{T}r_{\text{full}}, Tr \vdash \varphi} \Pr[Tr], \\
\Pr[Q \preceq \varphi] &= \sum_{Tr \in \mathcal{T}r_{\text{full}}, \exists Tr' \text{ prefix of } Tr, Tr' \vdash \varphi} \Pr[Tr] \\
&= \sum_{Tr \in \mathcal{T}r, 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\&v_m)) = \text{true}$ where the last configuration of $Tr$ is $Conf_m = E_m, (\sigma_m, P_m), Q_m, Ch_m, T_m, \mu\&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[Q : \varphi] \le \Pr[Q \preceq \varphi]$.

2. If $\varphi$ is preserved by extension, then $\Pr[Q : \varphi] = \Pr[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.7.3). The evaluation relation $E, \rho, M \Downarrow a$ can also be defined by induction as follows:

$$ \frac{E, \rho, i \Downarrow \rho(i)}{\frac{\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])}} \qquad \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)}{\frac{\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 a process $Q_0$, we write $I_\mu$ for the current replication indices at $\mu$ in $Q_0$.

**Lemma 2** Let $\mathbf{Tr}$ be a trace of $Q_0$. In the derivation of $\mathbf{Tr}$, for all configurations $E, \sigma, \mu M, \mathcal{T}, \mu \mathcal{E}v$ or $E, (\sigma, \mu P), \mathcal{Q}, \mathcal{Ch}, \mathcal{T}, \mu \mathcal{E}v$, $\mathrm{Dom}(\sigma) = I_\mu$ is the sequence of current replication indices at $\mu$ in $Q_0$ (or $\mathrm{Dom}(\sigma) = \emptyset$ is the sequence of current replication indices at $^{\mu \mathrm{start}}\langle\rangle$ in the initial configuration) and for all configurations $E, \mathcal{Q}, \mathcal{Ch}$ or $E, (\sigma, \mu P), \mathcal{Q}, \mathcal{Ch}, \mathcal{T}, \mu \mathcal{E}v$, for all $(\sigma', \mu' Q) \in \mathcal{Q}, \mathrm{Dom}(\sigma') = I_{\mu'}$.

**Proof sketch** We say that

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

* a configuration $E, \mathcal{Q}, \mathcal{Ch}$ is ok when for all $(\sigma', \mu' Q) \in \mathcal{Q}, \mathrm{Dom}(\sigma') = I_{\mu'}$;

* a configuration $E, (\sigma, \mu P), \mathcal{Q}, \mathcal{Ch}, \mathcal{T}, \mu \mathcal{E}v$ is ok when $\mathrm{Dom}(\sigma) = I_\mu$ (or $\mathrm{Dom}(\sigma) = \emptyset$ is the sequence of current replication indices at $^{\mu \mathrm{start}}\langle\rangle$ in the initial configuration) and for all $(\sigma', \mu' Q) \in \mathcal{Q}, \mathrm{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 $E_1, \mathcal{Q}_1, \mathcal{Ch}_1$ is ok, then all configurations $E, \sigma, M, \mathcal{T}, \mu \mathcal{E}v$ in the derivation of $E_1, \mathcal{Q}_1, \mathcal{Ch}_1 \rightsquigarrow E_2, \mathcal{Q}_2, \mathcal{Ch}_2$ are ok and $E_2, \mathcal{Q}_2, \mathcal{Ch}_2$ is ok;

3. if $E_1, \mathcal{Q}_1, \mathcal{Ch}_1$ is ok, then reduce($E_1, \mathcal{Q}_1, \mathcal{Ch}_1$) is ok and all configurations $E, \sigma, M, \mathcal{T}, \mu \mathcal{E}v$ or $E, \mathcal{Q}, \mathcal{Ch}$ and in the derivation of $E_1, \mathcal{Q}_1, \mathcal{Ch}_1 \rightsquigarrow^* \mathcal{Q}$ reduce($E_1, \mathcal{Q}_1, \mathcal{Ch}_1$) are ok;

4. if $E_1, (\sigma_1, P_1), \mathcal{Q}_1, \mathcal{Ch}_1, \mathcal{T}_1, \mu \mathcal{E}v_1$ is ok, then all configurations $E, \sigma, M, \mathcal{T}, \mu \mathcal{E}v$ or $E, \mathcal{Q}, \mathcal{Ch}, \mathcal{T}, \mu \mathcal{E}v$ in the derivation of $E_1, (\sigma_1, P_1), \mathcal{Q}_1, \mathcal{Ch}_1, \mathcal{T}_1, \mu \mathcal{E}v_1 \xrightarrow{p} E_2, (\sigma_2, P_2), \mathcal{Q}_2, \mathcal{Ch}_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. We use Property 1 in the case of input (Input).

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 (Output), we use Property 3. In all other cases, $\sigma$ is unchanged. We use Property 1 when evaluating terms, in conditions of find and get and in (Ctx).

Moreover, in the computation of initConfig($Q_0$), the configuration $\emptyset, \{(\sigma_0, Q_0)\}$, fc($Q$) is ok (the current replication indices at the root of $Q_0$ are empty), so by Property 3, initConfig($Q_0$) 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{\alpha}) : e]\dots]$ for some $k \in \mathbb{N}$ and $C_1, \dots, C_k$ contexts defined in Figure 6, 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 $E, Q, Ch \rightsquigarrow E', Q', Ch'$, then $E' = E$ and $Ch \subseteq Ch'$. For all configurations $E'', \sigma'', N'', T'', \mu\mathcal{E}v''$ in the derivation of $E, Q, Ch \rightsquigarrow E', Q', Ch'$, we have $E'' = E, T'' = \emptyset$, and $\mu\mathcal{E}v'' = \emptyset$.

If $E, (\sigma, P), Q, Ch, T, \mu\mathcal{E}v \xrightarrow{p} t E', (\sigma', P'), Q', Ch', 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'$, and $Ch \subseteq Ch'$.

* If $E, (\sigma, P), Q, Ch, T, \mu\mathcal{E}v \xrightarrow{p} t E', (\sigma', P'), Q', Ch', T', \mu\mathcal{E}v'$ is derived by (Output), then $T' = T, \mu\mathcal{E}v' = \mu\mathcal{E}v$, for all configurations $E'', Q'', Ch''$ in that derivation, $E'' = E$ and $Ch \subseteq Ch'' \subseteq Ch'$, and for all configurations $E'', \sigma'', N'', T'', \mu\mathcal{E}v''$ in that derivation, $E'' = E, \sigma''$ is an extension of $\sigma, T'' = \emptyset$, and $\mu\mathcal{E}v'' = \emptyset$.

* In all other cases, $Ch' = Ch, \sigma'$ is an extension of $\sigma$, and if the process $P'$ is not abort or of the form $C_0[C_1[\dots C_k[\text{event_abort} (\mu, \tilde{\alpha}) : e]\dots]]$ for some $C_0$ context defined in Figure 10, $k \in \mathbb{N}$, and $C_1, \dots, C_k$ contexts defined in Figure 6, then $\sigma' = \sigma$. For all configurations $E'', \sigma'', N'', T'', \mu\mathcal{E}v''$ in the derivation of $E, (\sigma, P), Q, Ch, T, \mu\mathcal{E}v \xrightarrow{p} t E', (\sigma', P'), Q', Ch', 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 $E, Q, Ch \rightsquigarrow E', Q', Ch'$ and $E, (\sigma, P), Q, Ch, T, \mu\mathcal{E}v \xrightarrow{p} t E', (\sigma', P'), Q', Ch', T', \mu\mathcal{E}v'$. $\square$

We say that a term $N$ is in evaluation position in a configuration $E, \sigma, M, 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 6.

An input context is a context of the form $^\mu c[a_1, \dots, a_{j-1}, [], M_{j+1}, \dots, M_m](x[\tilde{i}] : T); P$.
We say that a term $N$ is in *evaluation position* in a configuration $E, Q, Ch$ when $(\sigma', Q) \in Q$ and $Q = C_0[C_1[\dots C_k[N]\dots]]$ for some $C_0$ input context, $k \in \mathbb{N}$ and $C_1, \dots, C_k$ contexts defined in Figure 6.

We say that a term $N$ is *in evaluation position* in a configuration $E, (\sigma, P), Q, Ch, T, \mu\mathcal{E}v$ when $P = C_0[C_1[\dots C_k[N]\dots]]$ for some $C_0$ context defined in Figure 10, $k \in \mathbb{N}$, and $C_1, \dots, C_k$ contexts defined in Figure 6 or $(\sigma', Q) \in Q$ and $Q = C_0[C_1[\dots C_k[N]\dots]]$ for some $C_0$ input context, $k \in \mathbb{N}$ and $C_1, \dots, C_k$ contexts defined in Figure 6.

The output process $P$ is *in evaluation position* in configuration $E, (\sigma, P), Q, Ch, T, \mu\mathcal{E}v$. The input processes $Q$ such that $(\sigma', Q) \in Q$ for some $\sigma'$ are *in evaluation position* in configurations $E, Q, Ch$ and $E, (\sigma, P), Q, Ch, T, \mu\mathcal{E}v$.

**Lemma 4** Consider a trace Tr of $Q_0$.

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

All subterms and subprocesses of processes in $Q$ that occur in non-evaluation position in a configuration $E, Q, Ch$ in the derivation of Tr are subterms, resp. subprocesses, of $Q_0$ up to renaming of channels.

All subterms and subprocesses of $P$ and of processes in $Q$ that occur in non-evaluation position in a configuration $E, (\sigma, P), Q, Ch, T, \mu\mathcal{E}v$ in the derivation of Tr are subterms, resp. subprocesses, of $Q_0$ up to renaming of channels (except for the process 0 that follows $\overline{start}(\langle\rangle)$ in `initConfig($Q_0$)`).

**Proof** We say that

* a configuration $E, \sigma, M, 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 $E, Q, Ch$ is ok when all subterms and subprocesses of processes in $Q$ that are not in evaluation position are subterms, resp. subprocesses, of $Q_0$ up to renaming of channels;

* a configuration $E, (\sigma, P), Q, Ch, T, \mu\mathcal{E}v$ is ok when all subterms and subprocesses of $P$ and of processes in $Q$ that are not in evaluation position are subterms, resp. subprocesses, of $Q_0$ up to renaming of channels.

We show by induction on the derivations that

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

2. if $E_1, Q_1, Ch_1$ is ok, then all configurations $E, \sigma, M, T, \mu\mathcal{E}v$ in the derivation of $E_1, Q_1, Ch_1 \rightsquigarrow E_2, Q_2, Ch_2$ are ok and $E_2, Q_2, Ch_2$ is ok;

3. if $E_1, Q_1, Ch_1$ is ok, then reduce($E_1, Q_1, Ch_1$) is ok and all configurations $E, \sigma, M, T, \mu\mathcal{E}v$ or $E, Q, Ch$ and in the derivation of $E_1, Q_1, Ch_1 \rightsquigarrow^* \mu\mathcal{E}v(E_1, Q_1, Ch_1)$ are ok;

4. if $E_1, (\sigma_1, P_1), Q_1, Ch_1, T_1, \mu\mathcal{E}v_1$ is ok, then all configurations $E, \sigma, M, T, \mu\mathcal{E}v$ or $E, Q, Ch$ or $E, (\sigma, P), Q, Ch, T, \mu\mathcal{E}v$ in the derivation of $E_1, (\sigma_1, P_1), Q_1, Ch_1, T_1, \mu\mathcal{E}v_1 \xrightarrow{p} t E_2, (\sigma_2, P_2), Q_2, Ch_2, 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 processes in $Q$. This is enough to conclude for (Nil). For (Par) and (Repl), the resulting processes $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 channels. For (NewChannel), $Q$ is not in evaluation position in the initial configuration, so it is a subprocesses of $Q_0$ up to renaming of channels, and so is $Q\{c'/c\}$. For (Input), the subterms of $M_j$ that are not in evaluation position are not in evaluation position in $C[M_j]$, so they are subterms of $Q_0$. We can then apply Property 2 for the recursive call, so all configurations in the derivation of the recursive call are ok. The target configuration is ok because the subterms or subprocesses of $C[M_j']$ not in evaluation position are either subterms of $M'_j$ not in evaluation position, which are subterms of $Q_0$ since the target configuration is ok, or subterms of subprocesses of $C$ not in evaluation position, which are subterms or subprocesses of $Q_0$ up to renaming of channels.

Property 3 follows immediately from Property 2 by induction.

**Property 4:** In (Output), $Q''$ is not in evaluation position in the initial configuration, so it is a subprocess of $Q_0$ up to renaming of channels. Therefore, the configuration $E, \{(\sigma, Q'')\}, Ch$ is ok. By Property 3, all configurations in the computation of $E, Q', Ch'$ and $E, Q', Ch'$ itself are ok. Moreover, $P$ is not in evaluation position in the initial configuration, so it is a subprocess of $Q_0$ up to renaming of channels. We can then conclude that the target configuration is ok. All other cases can be treated similarly to terms in Property 1.

Moreover, in the computation of initConfig($Q_0$), the configuration $\emptyset, \{(\sigma_0, Q_0)\}, fc(Q)$ is ok, so by Property 3, initConfig($Q_0$) is ok except for the process 0 that follows $start\langle\rangle$ in initConfig($Q_0$). That process disappears in the first reduction, which is by (Output). $\square$

**Corollary 1** Consider a trace *Tr* of *Q*₀.

*In Tr*, the target process of rules (New), (Let), (If1), (If2), (Find1), (Find2), (Insert), (Get1), (Get2), (Output), (Event) is a subprocess of $Q_0$ up to renaming of channels.

*In 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 process 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 channels. $\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 $\text{Conf} = E, \sigma, \mu N, T, \mu \mathcal{E}v$ for some subterm $\mu N$ of $Q_0$ or $\text{Conf} = E, (\sigma, \mu P), Q, Ch, T, \mu \mathcal{E}v$ for some subprocess $\mu P$ of $Q_0$ up to renaming of channels.

**Lemma 5** Let Tr be a trace of $Q_0$. 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 process in the initial configuration of rules for find and get is always a subterm or subprocess of $Q_0$ up to renaming of channels. 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 $\text{Conf}_1 \xrightarrow{p} \text{Conf}_2$ occurs in the derivation of Tr, then $\text{Conf}_1 \leq_{Tr} \text{Conf}_2$ and for all Conf that occur in the derivation of the assumptions of $\text{Conf}_1 \xrightarrow{p} \text{Conf}_2$, $\text{Conf}_1 \leq_{Tr} \text{Conf} \leq_{Tr} \text{Conf}_2$, and similarly for $\rightsquigarrow$ instead of $\xrightarrow{p}$. If Tr is a trace of $Q_0$, then for all Conf that occur in the derivation of $\emptyset, \{(\sigma_0, Q_0)\}, \text{fc}(Q_0) \rightsquigarrow \emptyset, Q, Ch$, we have $\text{Conf} \leq_{Tr} \text{initConfig}(Q_0)$. When $\text{Conf}_1 \leq_{Tr} \text{Conf}_2$, we say that $\text{Conf}_1$ occurs before $\text{Conf}_2$ in Tr, or equivalently, that $\text{Conf}_2$ occurs after $\text{Conf}_1$ in Tr.

We say that a configuration $\text{Conf} = E, \sigma, \mu N, T, \mu \mathcal{E}v, \text{Conf} = E, (\sigma, \mu P), Q, Ch, T, \mu \mathcal{E}v, \text{Conf} = E, (\sigma, \mu' P), Q, Ch, T, \mu \mathcal{E}v$ with $(\sigma', \mu Q) \in Q$, or $\text{Conf} = E, Q, Ch$ with $(\sigma', \mu Q) \in Q$ is inside program point $\mu$. A configuration may be inside several program points: $\text{Conf} = E, Q, Ch$ is inside the program points of the input processes in $Ch, \text{Conf} = E, (\sigma, P), Q, Ch, T, \mu \mathcal{E}v$ is inside the program points of one output process (P) as well as the input processes in $Ch$.

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}\text{new } x[\tilde{i}] : 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} \leq n_{j1}, \dots, u_{jm_j}[\tilde{i}] = i_{jm_j} \leq n_{jm_j} \text{ such that}$$

$$\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}}N_j) \text{ else } ^{\mu_0}N'$$

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

$$^{\mu}\text{get}[\text{unique?}] \text{Tbl}(x_1[\tilde{i}] : T_1, \dots, x_l[\tilde{i}] : T_l) \text{ such that } ^{\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! i \leq n \mu_1 Q $$

$$ \mu^{\text{newChannel}} c; \mu_1 Q $$

$$ \mu c[\mu_1 M_1, \dots, \mu_l M_l](p); \mu_0 P $$

$$ \mu c[\mu_1 M_1, \dots, \mu_l M_l] \langle \mu_0 N \rangle; Q $$

$$ \mu^{\text{new}} x[\tilde{i}] : 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} \le n_{j1}, \dots, u_{jm_j}[\tilde{i}] = i_{jm_j} \le n_{jm_j} \text{ suchthat} \right. \\ \left. \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 \right) \text{ else } \mu_0 P $$

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

$$ \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 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 $Tr$ be a trace of $Q_0$. If $Conf$ is a configuration in $Tr$ inside program point $\mu$ and $\mu$ is a program point in $Q_0$, then either $Conf$ is at the program point $\mu$ at the top of $Q_0$, or there exists a configuration $Conf' \neq Conf$ such that $Conf' \preceq_{Tr} Conf$ and $Conf'$ is inside program point $\mu$ or inside the program point $\mu'$ immediately above $\mu$ in $Q_0$.

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

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

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

* $Conf = \text{initConfig}(Q_0) = \emptyset, (\sigma_0, \mu''\text{start}(\langle\rangle)), Q, Ch, \emptyset, \emptyset$. Since $\mu''$ is not in $Q_0$, $\mu$ is the program point of a process in $Q$. Then $Conf' = \emptyset, Q, Ch$ is also inside $\mu$ and $Conf' \preceq_{Tr} Conf$, by definition of $\preceq_{Tr}$.

* $Conf$ is the initial configuration of an assumption of a semantic rule. 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, (CtxT), (Ctx), and (Input), 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 rule (Output), $Conf = E, \{(\sigma, Q'')\}, Ch$, and the initial configuration of the conclusion of the rule (Output) is inside the program point $\mu'$ immediately above $\mu$.

* $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 (CtxT), 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 input processes, 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 process, then for rules (Par), (Repl), and (NewChannel), the initial configuration of the rule is inside the program point $\mu'$ immediately above $\mu$, and for rule (Input), the initial configuration of the rule is inside the same program point $\mu$. In the rules for output processes other than (Output), $Q$ is unchanged, so if $\mu$ is the program point of a process in $Q$, then the initial configuration of the rule is inside the same program point $\mu$. In rules (New), (Let), (If1), (If2), (Find1), (Find2), (Insert), (Get1), (Get2), and (Event), if $\mu$ is the program point of an output process, 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 rule (Output), if $\mu$ is the program point of a process in $Q$, then the initial configuration of the rule is inside the same program point $\mu$. If $\mu$ is the program point of a process in $Q'$, then the configuration $E, Q', Ch'$ in the assumption of the rule is inside the same program point $\mu$. 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$.

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$.

1. If $Conf = E, \sigma, C_m[\dots C_1[\mu^M]\dots]$, $T, \mu \in v$ 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 6, 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, T, \mu \in v$, itself proved by (CtxT).

2. If $Conf = E, (\sigma, C_0[C_m[\dots C_1[\mu^M]\dots]])$, $Q, Ch, T, \mu \in v$ is the target configuration of a semantic rule in $Tr$, where $\mu$ is a program point in $Q_0$, $C_0$ is a process context defined in Figure 10, $C_1, \dots, C_m$ are term contexts defined in Figure 6, 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, T, \mu \in v$, itself proved by (CtxT).

3. Let $Q = C_0[C_m[\dots C_1[\mu^M]\dots]]$ where $\mu$ is a program point in $Q_0$, $C_0$ is an input context, $C_1, \dots, C_m$ are term contexts defined in Figure 6, and $\mu^M$ is not a subterm of $Q_0$. If $Conf = E, \{(\sigma, Q) \uplus Q, Ch$ is target configuration of a semantic rule that affects $Q$ in $Tr$, then the reduction that yields Conf is obtained by one application of (Input) 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 \in 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), (Output), or (Event), because in this case, by Corollary 1, the process of Conf would be a subprocess of $Q_0$ up to renaming of channels, 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.

Property 3. The reduction that yields Conf cannot be obtained by (Par), (Repl), or (NewChannel), because in this case, by Lemma 4, since $Q$ occurs in non-evaluation position in the initial configuration of the rule, $Q$ would be a subprocess of $Q_0$ up to renaming of channels, so $^{\mu}M$ would be a subterm of $Q_0$. Therefore, Conf is the target configuration of (Input). 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 (Input) with context $C_0$. We conclude by Property 1. □

**Lemma 8** Let Tr be a trace of $Q_0$.

1. If Conf = $E, (\sigma, ^{\mu}P), Q, Ch, \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')$, $Q, Ch, \mathcal{T}', \mu\mathcal{E}v'$ where $^{\mu}P'$ is a subprocess of $Q_0$ up to renaming of channels, by (Ctx) any number of times.

2. If Conf = $E, \{(\sigma, ^{\mu}Q)\} \uplus Q, Ch$ 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' = $E, \{(\sigma, ^{\mu}Q')\} \uplus Q, Ch$ where $^{\mu}Q'$ is a subprocess of $Q_0$ up to renaming of channels, by (Input) any number of times.

3. If Conf = $E, (\sigma, C_0[\dots C_m[\mu M]\dots])$, $Q, Ch, \mathcal{T}, \mu\mathcal{E}v$ is a configuration in Tr where $\mu$ is a program point in $Q_0$, $C_0$ is a process context defined in Figure 10, and $C_1, \dots, C_m$ are term contexts defined in Figure 6, 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 Conf' = $E', (\sigma, C_0[\dots C_m[\mu M']\dots])$, $Q, Ch, \mathcal{T}', \mu\mathcal{E}v'$ under one application of (Ctx) with context $C_0$ and $m$ applications of (CtxT) with contexts $C_m, \dots, C_1$.
4. If $\text{Conf} = E, \{(\sigma, C_0[C_m[\dots C_1[\mu M]\dots]]\} \uplus Q, \text{Ch}$ is a configuration in $\text{Tr}$, where $\mu$ is a program point in $Q_0$, $C_0$ is an input context, and $C_1, \dots, C_m$ are term contexts defined in Figure 6, then we have

$$E, \sigma, \mu M', \emptyset, \emptyset \xrightarrow{p} t \dots \xrightarrow{p'} t' E, \sigma, \mu M, \emptyset, \emptyset$$

by (CtxT) any number of times, where $\mu M'$ is a subterm of $Q_0$ and possibly after swapping reductions in $\text{Tr}$, these reductions are in fact performed starting from a configuration $\text{Conf}' = E, \{(\sigma, C_0[C_m[\dots C_1[\mu M']\dots]]\} \uplus Q, \text{Ch}$ under one application of (Input) with context $C_0$ and $m$ applications of (CtxT) with contexts $C_m, \dots, C_1$.

5. If $\text{Conf} = E, \sigma, C_l[\dots C_1[\mu M]\dots]$, $\mathcal{T}, \mu\mathcal{E}v$ is a configuration in $\text{Tr}$ and $\mu$ is a program point in $Q_0$ where $C_1, \dots, C_l$ are term contexts defined in Figure 6, 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 $\text{Tr}$, these reductions are in fact performed starting

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

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

* or, possibly after swapping reductions in $\text{Tr}$, from a configuration $\text{Conf}' = E', \{(\sigma, C_0[C_m[\dots C_1[\mu M']\dots]]\} \uplus Q, \text{Ch}$ where $m \ge l, C_0$ is an input context and $C_1, \dots, C_m$ are term contexts defined in Figure 6, under one application of (Input) 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 $\text{Conf}$ cannot be $\text{initConfig}(Q_0)$ because $\mu$ is a program point in $Q_0$. Then, $\text{Conf}$ is the target configuration of some semantic rule. If $\text{Conf}$ is the target configuration of (New), (Let), (If1), (If2), (Find1), (Find2), (Insert), (Get1), (Get2), (Output), or (Event), then by Corollary 1, $\mu P$ is a subprocess of $Q_0$ up to renaming of channels, so the property holds with $\text{Conf}' = \text{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 $\text{Conf} = \emptyset, \{(\sigma_0, Q_0)\}$, $\text{fc}(Q_0)$, then the property holds with $\text{Conf}' = \text{Conf}$, since $Q_0$ is a subprocess of $Q_0$. If $\text{Conf}$ is the initial configuration of the assumption of (Output), then by Lemma 4, $Q$ is a subprocess of $Q_0$ up to renaming of channels, since $Q$ occurs in non-evaluation position in the initial configuration of (Output). So the property holds with $\text{Conf}' = \text{Conf}$. Otherwise, $\text{Conf}$ is the target configuration of a semantic rule.

* If that rule does not affect $Q$, then it is of the form $E, \{(\sigma, \mu Q)\} \uplus Q', \text{Ch}' \rightsquigarrow E, \{(\sigma, \mu Q)\} \uplus Q, \text{Ch}$. We apply the induction hypothesis to $E, \{(\sigma, \mu Q)\} \uplus Q', \text{Ch}'$, so possibly after swapping reductions in $\text{Tr}$, we have $E, \{(\sigma, \mu Q')\} \uplus Q', \text{Ch}' \rightsquigarrow^* E, \{(\sigma, \mu Q)\} \uplus Q', \text{Ch}'$ by (Input) any number of times, where $\mu Q'$ is a subprocess of $Q_0$ up to renaming of channels. By swapping reductions, we have $E, \{(\sigma, \mu Q')\} \uplus Q', \text{Ch}' \rightsquigarrow E, \{(\sigma, \mu Q')\} \uplus Q, \text{Ch} \rightsquigarrow^* E, \{(\sigma, \mu Q)\} \uplus Q, \text{Ch}$, so we obtain the desired property with $\text{Conf}' = E, \{(\sigma, \mu Q')\} \uplus Q, \text{Ch}$.
* Otherwise, that rule affects $Q$. If that rule is (Par), (Repl), or (NewChannel), then by Lemma 4, $Q$ is a subprocess of $Q_0$ up to renaming of channels, 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 (Input), 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$) 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$, ..., $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.** Let $Q = C_0[C_m[\dots C_1[^\mu M]\dots]]$. The proof proceeds by well-founded induction on $\leq_{Tr}$. If $Conf = \emptyset, \{(\sigma_0, Q_0)\}, fc(Q_0)$, then the property holds with $Conf' = Conf$, since $Q_0$ is a subprocess of $Q_0$, so $^\mu M$ is a subterm of $Q_0$. If $Conf$ is the initial configuration of the assumption of (Output), then by Lemma 4, $Q$ is a subprocess of $Q_0$ up to renaming of channels, since $Q$ occurs in non-evaluation position in the initial configuration of (Output). So $^\mu M$ is a subterm of $Q_0$ and the property holds with $Conf' = Conf$. Otherwise, $Conf$ is the target configuration of a semantic rule. If that rule does not affect $Q$, then we swap reductions as in the proof of Property 2. Otherwise, if $^\mu M$ is a subterm of $Q_0$, then the property holds with $Conf' = Conf$. Otherwise, by Lemma 7, Property 3, the reduction that yields $Conf$ is obtained by one application of (Input) with context $C_0$ and $m$ applications of (CtxT) with contexts $C_m$, ..., $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 (Input).

**Property 5.** The proof proceeds by well-founded induction on $\leq_{Tr}$. 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 (CtxT), 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 (Input), we let $m = l$. The initial configuration of the rule is of the form $E, \{C_0[C_l[\dots C_1[^\mu M]\dots]]\} \uplus Q, Ch$ for some input context $C_0$. We conclude by applying Property 4 to that configuration. In (Ctx), 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, Ch, T, \mu\mathcal{E}v$ for some process context $C_0$ defined in Figure 10. 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 (CtxT) 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 (CtxT). 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 (Ctx) or (Input) with context $C_0$, (CtxT) $m$ times with contexts $C_m, \dots, C_1$ under the reduction with target configuration $E, \sigma, ^\mu M, T, \mu\mathcal{E}v$. Up to swapping of reductions in the case of input processes, this is also what happens in $Tr$. (By inspection of the rules, only the rule (Input) with context $C_0$ can reduce an input process $C_0[N]$, where $C_0$ is an input context; only the rule (Ctx) with context $C_0$ can
reduce an output process $C_0[N]$, where $C_0$ is a process context defined in Figure 10; only the rule (CtxT) with context $C_j$ can reduce a term $C_j[N]$, where $C_j$ is a term context defined in Figure 6.) □

### 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}\text{new } x[\tilde{i}] : T; N) = \{x[\sigma(\tilde{i})]\} \cup Defined(\sigma, N)$$

$$Defined(\sigma,^{\mu}\text{let } x[\tilde{i}] : T = M \text{ in } N) = \{x[\sigma(\tilde{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[\tilde{i}] = \tilde{i}_j \le \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} \le \tilde{n}_j} Defined(\sigma[\tilde{i}_j \mapsto \tilde{a}], M_j), \max_{j=1}^{m} \{\tilde{u}_j[\sigma(\tilde{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)$$

$$Defined(\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') = \\ \max(\{x_j[\sigma(\tilde{i})] | j \le l\} \cup \max(Defined(\sigma, M), Defined(\sigma, N)), Defined(\sigma, N'))$$

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

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

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

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

$$Defined(\sigma,^{\mu}(Q_1 | Q_2)) = Defined(\sigma, Q_1) \cup Defined(\sigma, Q_2)$$

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

$$Defined(\sigma,^{\mu}\text{newChannel } c; Q) = Defined(\sigma, Q)$$

$$Defined(\sigma,^{\mu}c[M_1, \dots, M_l](x[\tilde{i}] : T); P) = \{x[\sigma(\tilde{i})]\} \cup Defined(\sigma, P)$$

$$Defined(\sigma,^{\mu}\overline{c[M_1, \dots, M_l]}(N); Q) = \bigcup_{j=1}^{l} Defined(\sigma, M_j) \cup Defined(\sigma, N) \cup Defined(\sigma, Q)$$

$$Defined(\sigma,^{\mu}\text{new } x[\tilde{i}] : T; P) = \{x[\sigma(\tilde{i})]\} \cup 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{) = } \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) \land M_j \text{ then } P_j) \text{ else } P) = \\ \max(\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)) $$

$$ \text{Defined}(\sigma, \mu)\text{insert } 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?}] 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 $$

Notice that, by Invariant 5, the terms $M_j$ in channels of inputs and 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, T, \mu\mathcal{E}v$ or $Conf = E, (\sigma, P), Q, Ch, T, \mu\mathcal{E}v$ or $Conf = E, Q, Ch$, we denote by $E_{Conf}$ the environment $E$ in configuration $Conf$. We define

$$ \text{Defined}^{\text{Fut}}(E, \sigma, M, T, \mu\mathcal{E}v) = \text{Defined}(\sigma, M) $$

$$ \text{Defined}^{\text{Fut}}(E, Q, Ch) = \bigcup_{(\sigma, Q) \in \mathcal{Q}} \text{Defined}(\sigma, Q) $$

$$ \text{Defined}^{\text{Fut}}(E, (\sigma, P), Q, Ch, T, \mu\mathcal{E}v) = \text{Defined}(\sigma, P) \uplus \bigcup_{(\sigma, Q) \in \mathcal{Q}} \text{Defined}(\sigma, Q) $$

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

**Invariant 8 (Single definition, for executing games)** The semantic configuration $Conf$ (which can be $E, \sigma, M, T, \mu\mathcal{E}v$ or $E, Q, Ch$ or $E, (\sigma, P), Q, Ch, T, \mu\mathcal{E}v$) satisfies Invariant 8 if and only if $Defined(Conf)$ does not contain duplicate elements.

**Lemma 9** Let $Tr$ be trace of $Q_0$. If $Q_0$ satisfies Invariant 1, then all semantic configurations in the derivation of $Tr$ satisfy Invariant 8.

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

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

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

The result follows: since $Q_0$ satisfies Invariant 1, $Defined(\sigma_0, Q_0)$ does not contain duplicate elements, where $\sigma_0$ is the empty mapping sequence. Then $\emptyset, \{(\sigma_0, Q_0)\}, fc(Q_0)$ satisfies Invariant 8 and so do reduce($\emptyset, \{(\sigma_0, Q_0)\}, fc(Q_0)$), initConfig($Q_0$), and the other configurations of $Tr$.

□

**Corollary 2** If $Q_0$ 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_0$.

**Proof** Let $x$ be the considered variable and $Tr$ be the considered trace of $Q_0$. The only semantic rules that can add $x[\tilde{a}]$ to the environment $E$ are (NewT), (LetT), (FindT1), (GetT1), (New), (Let), (Find1), (Get1), and (Output). By Corollary 1, the target term or process of these rules is a subterm or subprocess of $Q_0$ up to renaming of channels. Hence, the target configuration $Conf'$ of these rules is at some program point $\mu$ in $Tr$. By hypothesis, $x$ is not defined in conditions of find or get, so $\mu$ is not inside the condition of find or get in $Q_0$, 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_{Tr} Conf_2$. (The case $Conf'_2 \preceq_{Tr} 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 $Defined(Conf_2) = \text{Dom}(E_{Conf_2}) \uplus Defined^{\text{Fut}}(Conf_2)$ contains twice $x[\tilde{a}]$. Contradiction with Invariant 8.

* Second case: the transitions cannot be ordered. By definition of $\preceq_{Tr}$, 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.6, we define properties that exclude these situations (Properties 4 and 5), and we prove in Lemma 28 that every variable is defined at most once for each value of its indices when these properties are satisfied.
### 2.4.4 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 9 (Defined variables, for executing games)** The semantic configuration $E, (\sigma, P), Q, Ch, T, \mu\mathcal{E}v$ satisfies Invariant 9 if and only if every occurrence of a variable access $x[M_1, \dots, M_m]$ in $(\sigma, P)$ or $Q$ is either

1. present in $\text{Dom}(E)$: if $x[M_1, \dots, M_m]$ occurs in a process $P'$ for $(\sigma', P') \in \{(\sigma, P)\} \cup Q$, then for all $j \le m$, $E, \sigma', M_j \downarrow a_j$ and $x[a_1, \dots, a_m] \in \text{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[i] = \tilde{i}_j \le \tilde{n}_j$ such that defined($M'_{j1}, \dots, M'_{j_l}$) $\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}$.

5. or in $P_j$ in a process or term of the form find ($\bigoplus_{j=1}^{m''} \tilde{u}_j[i] = \tilde{i}_j \le \tilde{n}_j$ such that defined($M'_{j1}, \dots, M'_{j_l}$) $\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[i]/\tilde{i}_j\} = x[M_1, \dots, M_m]$.

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

$E, \sigma, \text{defined}(M'_1, \dots, M'_l) \land M, T, \mu\mathcal{E}v$ satisfies Invariant 9 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 $\text{Dom}(E)$ (for all $j \le m$, $E, \sigma, M_j \downarrow a_j$ and $x[a_1, \dots, a_m] \in \text{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 \downarrow a_j$.

**Lemma 10** If $Q_0$ satisfies Invariant 2, then $\text{initConfig}(Q_0)$ satisfies Invariant 9.

**Lemma 11** Let $M$ be a simple term. If $E, \sigma, M \downarrow a$, then for all subterms $x[M_1, \dots, M_m]$ of $M$, for all $j' \le m$, $E, \sigma, M_{j'} \downarrow a_{j'}$ and $x[a_1, \dots, a_m]$ is in $\text{Dom}(E)$.

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

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

**Lemma 12** 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$

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

**Lemma 13** If $E, \sigma, M, T, \mu\mathcal{E}v \stackrel{p}{\to}_t E', \sigma', M', T', \mu\mathcal{E}v'$ and $E, \sigma, M, T, \mu\mathcal{E}v$ satisfies Invariant 9, then so does $E', \sigma', M', T', \mu\mathcal{E}v'$.

If $E, \sigma, \text{defined}(M_1, \dots, M_m) \land M, T, \mu\mathcal{E}v \stackrel{p}{\to}_t E', \sigma', M', T', \mu\mathcal{E}v'$ and $E, \sigma, \text{defined}(M_1, \dots, M_m) \land M, T, \mu\mathcal{E}v$ satisfies Invariant 9, then so does $E', \sigma', M', T', \mu\mathcal{E}v'$.
If $E, (\sigma, P), Q, Ch, T, \mu\mathcal{E}v \xrightarrow{p} t E', (\sigma', P'), Q', Ch', T', \mu\mathcal{E}v'$ and $E, (\sigma, P), Q, Ch, T, \mu\mathcal{E}v$ satisfies Invariant 9, then so does $E', (\sigma', P'), Q', Ch', T', \mu\mathcal{E}v'$.

Moreover, if the rules that define $E, \sigma, M, T, \mu\mathcal{E}v \xrightarrow{p} t E', \sigma', M', T', \mu\mathcal{E}v'$ (resp. $E, \sigma, \text{defined}(M_1, \dots, M_m) \wedge M, T, \mu\mathcal{E}v \xrightarrow{p} t E', \sigma', M', T', \mu\mathcal{E}v'$ or $E, (\sigma, P), Q, Ch, T, \mu\mathcal{E}v \xrightarrow{p} t E', (\sigma', P'), Q', Ch', T', \mu\mathcal{E}v'$) require as assumption $E'', \sigma'', M'', T'', \mu\mathcal{E}v'' \xrightarrow{p} t \dots$ or $E'', \sigma''$, $\text{defined}(M_1'', \dots, M_m'') \wedge M'', T'', \mu\mathcal{E}v'' \xrightarrow{p} t \dots$, and the initial configuration $E, \sigma, M, T, \mu\mathcal{E}v$ (resp. $E, \sigma, \text{defined}(M_1, \dots, M_m) \wedge M, T, \mu\mathcal{E}v$ or $E, (\sigma, P), Q, Ch, T, \mu\mathcal{E}v$) satisfies Invariant 9, then so does the initial configuration of the assumption, $E'', \sigma'', M'', T'', \mu\mathcal{E}v''$ or $E'', \sigma''$, $\text{defined}(M_1'', \dots, M_m'') \wedge M'', 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 9, 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), (Output), or (Get1) so it moves to the first case of Invariant 9.

If $x[M_1, \dots, M_m]$ is in the third case of Invariant 9, 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 9, 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, T, \mu\mathcal{E}v \xrightarrow{p_{k'}} E'', \sigma', r_{k'}, 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 9. In case this assumption is reduced by (DefinedYes), we have $E, \sigma', M'_{jk}, T, \mu\mathcal{E}v \xrightarrow{1^*} E, \sigma', a_{jk}, T, \mu\mathcal{E}v$, that is, $E, \sigma', M'_{jk} \triangleleft a_{jk}$. Therefore, by Lemma 11, for all $j' \le m$, $E, \sigma', M'_{j'} \triangleleft 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 9 in $E, \sigma', M'_{j'}, T, \mu\mathcal{E}v$ after reduction by (DefinedYes).

If $x[M_1, \dots, M_m]$ is in the last case of Invariant 9, 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, T, \mu\mathcal{E}v \xrightarrow{p_{k'}} E, \sigma', r_{k'}, 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}, T, \mu\mathcal{E}v \xrightarrow{1^*} E, \sigma', a, T, \mu\mathcal{E}v$ for some $a$, that is, $E, \sigma', M'_{jk} \triangleleft a$. The term $N = x[N_1, \dots, N_m]$ is a subterm of $M'_{jk}$. Therefore, by Lemma 11, for all $j' \le m$, $E, \sigma', N'_{j'} \triangleleft a'_{j'}$ and $x[a_1, \dots, a_m]$ is in $\text{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 $\text{Dom}(E')$. We have for all $j' \le m$, $M'_{j'} = N'_{j'}\{\tilde{u}_j[\tilde{i}]/\tilde{i}_j\}$, $E'(\tilde{u}_j[\tilde{i}]) = \tilde{a}'$, and $\sigma'(\tilde{i}_j) = \tilde{a}'$, so by Lemma 12, for all $j' \le m$, $E', \sigma, M'_{j'} \triangleleft a'_{j'}$ and $x[a_1, \dots, a_m]$ is in $\text{Dom}(E')$. So $x[M_1, \dots, M_m]$ also moves to the first case of Invariant 9.

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. $\square$

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 \Downarrow 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.5 Typing

In this section, we show that our type system is compatible with the semantics of the calculus, 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$, $\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}$. (These rules are useful to type evaluated terms and processes.)

* $\mathcal{E} \vdash (\sigma, P)$ if and only if $\mathcal{E}[i_1 \mapsto [1, n_1], \dots, i_m \mapsto [1, n_m]] \vdash P$ 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, Q)$ and $\mathcal{E} \vdash (\sigma, M): T$ are defined in the same way.

* $\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, P)$, $Q$, $Ch$, $\mathcal{T}$, $\mu\mathcal{E}v$ if and only if $\mathcal{E} \vdash E$, $\mathcal{E} \vdash (\sigma, P)$, $\mathcal{E} \vdash \mathcal{T}$, $\mathcal{E} \vdash \mu\mathcal{E}v$, and for all $(\sigma', Q) \in Q$, $\mathcal{E} \vdash (\sigma', Q)$.

* $\mathcal{E} \vdash E$, $Q$, $Ch$ if and only if $\mathcal{E} \vdash E$ and for all $(\sigma', Q) \in 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 14** If $\mathcal{E} \vdash E$, $\sigma$, $M: T$, $\mathcal{T}$, $\mu\mathcal{E}v$ and $E$, $\sigma$, $M$, $\mathcal{T}$, $\mu\mathcal{E}v \xrightarrow{p} 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 \xrightarrow{p^*} T$ $E'$, $\sigma'$, $a$, $T'$, $\mu\mathcal{E}v'$, then $\mathcal{E} \vdash E'$, $\sigma'$, $a: T$, $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'$.

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

**Lemma 15** If $\mathcal{E} \vdash E$, $Q$, $Ch$ and $E$, $Q$, $Ch \rightsquigarrow E'$, $Q'$, $Ch'$, then $\mathcal{E} \vdash E'$, $Q'$, $Ch'$.

So, if $\mathcal{E} \vdash E$, $Q$, $Ch$, then $\mathcal{E} \vdash \text{reduce}(E, Q, Ch)$.

**Proof sketch** By cases on the derivation of $E, Q, Ch \rightsquigarrow E'$, $Q'$, $Ch'$. In the case of the replication, we have $\mathcal{E} \vdash (\sigma, !^{i \le n} Q)$, so $\mathcal{E}[i_1 \mapsto [1, n_1], \dots, i_m \mapsto [1, n_m]] \vdash !^{i \le n} 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]$. In the case of the input, we use Lemma 14.

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

**Lemma 16** If $\mathcal{E} \vdash Q_0$, then $\mathcal{E} \vdash \text{initConfig}(Q_0)$.
**Proof sketch** By Lemma 15 and the previous definitions. □

**Lemma 17 (Subject reduction)** If $\mathcal{E} \vdash E, (\sigma, P), Q, Ch, T, \mu\mathcal{E}v$ and $E, (\sigma, P), Q, Ch, T, \mu\mathcal{E}v \xrightarrow{p} t E', (\sigma', P'), Q', Ch', T', \mu\mathcal{E}v', \text{ then } \mathcal{E} \vdash E', (\sigma', P'), Q', Ch', T', \mu\mathcal{E}v'$.

**Proof sketch** By cases on the derivation of $E, P, Q, Ch, T, \mu\mathcal{E}v \xrightarrow{p} t E', (\sigma', P'), Q', Ch', T', \mu\mathcal{E}v'$, using Lemmas 14 and 15. □

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

As an immediate consequence of Lemmas 16, 17, and 14 and the observation above, we obtain: if $Q_0$ satisfies Invariant 7, 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 $bool = \{\text{false, true}\}$ (when it is a value, not an abort event value), so the condition $a \ne \text{true}$ is equivalent to $a = \text{false}$. In the rules for *find*, we have $r_k \in \{\text{false, 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 $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$.

## 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 channels $c$ are used without indices, and the current replication indices are implicitly added by CryptoVerif. This allows the adversary to select to which copy of processes it sends messages. The construct *newChannel* cannot occur in games manipulated by CryptoVerif. It is used only inside proofs. The grammar of the resulting calculus is summarized in Figure 11.

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 indices at the definition of $x$. Such accesses are simply abbreviated as $x$. Variables can then be considered as ordinary variables instead of arrays, since we only access the array cell at the current replication indices. This choice has several other advantages:

* Tables with *get/insert* are closer to lists usually used by cryptographers than *find*, they should be easier to understand for the user.

* Tables are supported by the symbolic protocol verifier ProVerif while *find* is not. Similarly, ProVerif does not support channels with indices. So avoiding *find* and channels with indices allows us to have a language compatible with ProVerif.

* Our compiler that translates CryptoVerif specifications into OCaml implementations [28] does not support *find*, because tables with *get/insert* are also much easier to implement than *find*.
<figure><img src="image_9.png" /><figcaption>Figure 11: Subset of the calculus for the initial game</figcaption></figure>
We can define processes by macros: let pid($x_1$: $T_1$, ..., $x_m$: $T_m$) = P or let qid($x_1$: $T_1$, ..., $x_m$: $T_m$) = Q. If a process pid($M_1$, ..., $M_m$) occurs in the initial game, CryptoVerif verifies that $M_1$, ..., $M_m$ are of types $T_1$, ..., $T_m$ respectively, and replaces pid($M_1$, ..., $M_m$) with the expansion $P\{M_1/x_1, ..., M_m/x_m\}$.

We can also define functions by macros: letfun $f(x_1$: $T_1$, ..., $x_m$: $T_m$) = M. If a term $f(M_1, ..., M_m)$ occurs in the initial game, CryptoVerif verifies that $M_1$, ..., $M_m$ are of types $T_1, ..., T_m$ respectively, and replaces $f(M_1, ..., M_m)$ with the expansion $M\{M_1/x_1, ..., M_m/x_m\}$.

In the initial game, all bound variables with several incompatible definitions (different indices, different types, or variables defined in the same branch of a test) as well as variables declared without an explicit type are not allowed to occur in V nor in defined conditions of find or if and are renamed to distinct names, so that Invariant 1 is satisfied for these variables. The condition on input channels in Invariant 5 is always satisfied by definition of the language. CryptoVerif checks the rest of the invariants.

## 2.6 Subsets used inside the Sequence of Games

During the computation of the sequence of games, several properties are used by CryptoVerif, either required by some game transformations or guaranteed by others. We summarize them in this section.

**Property 1** No function returns values of interval types. The types of values chosen by new $x[\tilde{i}]$: $T$ are not interval types. The type $T$ of the sent message in the (TOut) rule and of the receiving pattern in the (TIn) rule are not interval types.

This property is satisfied by all games manipulated by CryptoVerif, but not by processes that model the adversary. Combined with Invariants 7, 2, and 5, it implies that the terms of variable accesses $x[M_1, ..., M_m]$ contain only replication indices and variables. (Tuples, events, and tables can take interval types as arguments. The constraint on inputs and outputs could probably be relaxed.)

For processes that model security assumptions on primitives, the receiving variable can be of an interval type. (This is used for instance to specify the computational Diffie-Hellman assumption; see Section 5.2.)

**Property 2** The newChannel $c$ construct does not appear in games.

**Property 3** The indices of channels are always the current replication indices.

These properties are also satisfied by all games manipulated by CryptoVerif, but not by processes that model the adversary.

**Property 4** The constructs insert and get do not occur in the game.

This property is not valid in the initial game, but it is in all other games of the sequence produced by CryptoVerif. The very first game transformation applied by CryptoVerif, expand_tables, encodes insert and get using find (see Section 5.1.2). The constructs insert and get are never introduced by subsequent game transformations, so this property remains valid in the rest of the sequence.

**Property 5** The variables defined in conditions of find have pairwise distinct names.
<figure><img src="image_10.png" /><figcaption>Figure 12: Subset after game expansion</figcaption></figure>
This property is enforced by the transformation **auto_SArename** (see Section 5.1.2) by renaming variables defined in conditions of find to distinct names. (This is easy since these variables do not have array accesses by Invariant 3.) Property 5 is required as a precondition by many game transformations, and may be broken by game transformations that duplicate code. Therefore, we apply **auto_SArename** after these game transformations.

**Property 6** The terms *M* are simple except for conditions of find.

The grammar of the language taking into account this property as well as Properties 2 and 4 is shown in Figure 12. By Invariant 4, event does not occur in conditions of find, so event never occurs as term. Property 6 is enforced by the transformation **expand** (see Section 5.1.3) by converting other terms into processes. This transformation is applied on the initial game after **expand_tables**. Property 6 is broken by the cryptographic transformation of Section 5.2, so by default **expand** is called again after this transformation. Many game transformations require Property 6 as a precondition.

## 2.7 Security Properties, Indistinguishability

A context is a process containing a hole []. An evaluation context *C* is a context built from [], newChannel *c*; *C*, *Q* | *C*, and *C* | *Q*. We use an evaluation context to represent the adversary. We denote by *C*[*Q*] the process obtained by replacing the hole [] in the context *C* with the process *Q*.

We write event(*D*) for the set of events that occur in the distinguisher *D* (i.e. are used by the distinguisher *D*). We write event(*Q*) for the set of events that occur in the process *Q*. We use similar notations for output processes, contexts, ... We write event(*Q*, *Q*') for event(*Q*) ∪ event(*Q*').

**Definition 5 (Indistinguishability)** Let *Q* and *Q'* be two processes, *V* a set of variables, and *E* a set of events. Assume that *Q* and *Q'* satisfy Invariants 1 to 7 with public variables *V*, and the variables of *V* are defined in *Q* and *Q*', with the same types.

An evaluation context *C* is said to be *acceptable* for *Q* with public variables *V* if and only if var(*C*) ∩ var(*Q*) ⊆ *V*, vardef(*C*) ∩ *V* = ∅, *C* and *Q* do not use any common table, and *C*[*Q*] satisfies Invariants 1 to 7 with public variables *V*.

We write $Q \approx_{p, \mathcal{E}} Q'$ when, for all evaluation contexts $C$ acceptable for $Q$ and $Q'$ with public variables $V$ and all distinguishers $D$ that run in time at most $t_D$ and such that $\text{event}(D) \cap \text{event}(Q, Q') \subseteq \mathcal{E}$, $|\Pr[C[Q] : D] - \Pr[C[Q'] : D]| \le p(C, t_D)$.

This definition formalizes that the probability that algorithms *C* and *D* distinguish the games *Q* and *Q'* is at most *p*(*C*, *t*<sub>*D*</sub>). The probability *p* typically depends on the runtime of *C* and *D*, but may also depend on other parameters, such as the number of queries to each oracle made by *C*. That is why *p* takes as arguments the whole algorithm *C* and the runtime of *D*. More specifically:

**Property 7** All probabilities computed by CryptoVerif are built from the following components by mathematical operations:

* the runtime of the context;

* the maximum number of outputs made by the context on each channel;

* the value of replication bounds, which is also determined from the number of outputs performed by the context on channels;
* the maximum length of the bitstring represented by a term, in particular a variable; this length may depend on messages output by the context; it is used only for unbounded types; for bounded types, we use the maximum length of the type instead;

* the maximum length of bitstring of a type $T$;

* the length of the result of a function, expressed as a function of the length of its arguments;

* the time of some action, expressed as a function of other elements of the formula;

* probability functions, used in particular to express the probability of breaking each primitive from other elements of the formula;

* the cardinal $|T|$ of a type $T$;

* the probability of collision between two random values of a type $T$, or between a random value and a value independent from that random value; these probabilities depend on the default distribution on the type $D_T$;

* $\epsilon_T$, the distance between the default distribution $D_T$ of type $T$ and the uniform distribution;

* $\epsilon_{find}$, where the distance between $D_{find}(S)$ and the uniform distribution is $\epsilon_{find}/2$.

Among the elements above, the first four depend on the context. In particular, probability formulas output by CryptoVerif do not depend on the variable, table, event names in the context. They also do not depend on the values of variables, but may depend on their length. For variables of bounded types, the probabilities do not depend at all on the values.

The set of events $\mathcal{E}$ corresponds to events that the adversary is allowed to observe. When $\mathcal{E} = \text{event}(Q, Q')$, we omit it and write $Q \approx_p^{\mathcal{E}} Q'$.

The unusual requirement on variables of $C$ comes from the presence of arrays and of the associated find construct which gives $C$ direct access to variables of $Q$ and $Q'$: the context $C$ is allowed to access variables of $Q$ and $Q'$ only when they are in $V$. (In more standard settings, the calculus does not have constructs that allow the context to access variables of $Q$ and $Q'$.) When $V$ is empty, we omit it and write $Q \approx_p^{\mathcal{E}} Q'$.

When $C$ is acceptable for $Q$ with public variables $V$, and we transform $Q$ into $Q'$, we can rename the fresh variables of $Q'$ (introduced by the game transformation) so that they do not occur in $C$. Then $C$ is also acceptable for $Q'$ with public variables $V$. (To establish this property, we use that the variables of $V$ are defined in $Q$ and $Q'$, with the same types, so that, if $C[Q]$ is well-typed, then so is $C[Q']$.)

When $C$ is acceptable for $Q$ with public variables $V$, we have that $\text{vardef}(C) \cap \text{var}(Q) = \emptyset$, because $\text{vardef}(C) \cap \text{var}(Q) = \text{vardef}(C) \cap \text{var}(C) \cap \text{var}(Q) \subseteq \text{vardef}(C) \cap V = \emptyset$.

The following lemma is a straightforward consequence of Definition 5:

**Lemma 18** 1. Reflexivity: $Q \approx_0^{V, \mathcal{E}} Q$.

2. Symmetry: If $Q \approx_p^{V, \mathcal{E}} Q'$, then $Q' \approx_p^{V, \mathcal{E}} Q$.

3. Transitivity: If $Q \approx_p^{V, \mathcal{E}} Q'$ and $Q' \approx_{p'}^{V, \mathcal{E}} Q''$, then $Q \approx_{p+p'}^{V, \mathcal{E}} Q''$.

4. Application of a context: If $Q \approx_p^{V, \mathcal{E}} Q'$ and $C$ is an evaluation context acceptable for $Q$ and $Q'$ with public variables $V$, then $C[Q] \approx_{p', \mathcal{E}}^{V', \mathcal{E}} C[Q']$, where $p'(C', t_D) = p(C'[C}], t_D)$, $V' \subseteq V \cup \text{var}(C)$, and $\mathcal{E}' = \mathcal{E} \cup (\text{event}(C) \setminus \text{event}(Q, Q'))$.
Next, we introduce a notion related to indistinguishability that treats Shoup and non-unique events specially.

**Definition 6 (Property preservation with introduction of events)** Let $Q$ and $Q'$ be two processes and $V$ a set of variables. Assume that $Q$ and $Q'$ satisfy Invariants 1 to 7 with public variables $V$, and the variables of $V$ are defined in $Q$ and $Q'$, with the same types.

Let $D_{\text{false}}(\mathcal{E}v) = \text{false for all } \mathcal{E}v$. Let $\text{NonUnique}_Q = \bigvee\{e \mid [\text{unique}_e] \text{ occurs in } Q\}$ and $\text{NonUnique}_{Q,D} = \bigvee\{e \mid [\text{unique}_e] \text{ occurs in } Q, e \notin D\}$, where $D$ is a distinguisher consisting of a disjunction of Shoup and non-unique events, and we write $e \notin D$ to say that $e$ does not occur in this disjunction. We have $\text{NonUnique}_{Q,D} = \text{NonUnique}_Q \wedge \neg D$.

We write $\mathcal{D}, \mathcal{D}_{\text{SNU}} : Q, D, \text{EvUsed} \xrightarrow{V} p Q', D', \text{EvUsed}'$ when $\mathcal{D}$ is a set of distinguishers, $\mathcal{D}_{\text{SNU}}$ is a set of Shoup and non-unique events in $\text{EvUsed}$, $D$ and $D'$ are distinguishers consisting of a disjunction of Shoup and non-unique events, the events that occur in $Q$ or in $D$ are in $\text{EvUsed}$, $\text{EvUsed} \subseteq \text{EvUsed}'$, the events that occur in $Q'$ but not in $Q$ are in $\text{EvUsed}'$ but not in $\text{EvUsed}$, the events that occur in $D'$ but not in $D$ are in $\text{EvUsed}'$ but not in $\text{EvUsed}$, and, for all evaluation contexts $C$ acceptable for $Q$ and $Q'$ with public variables $V$ that do not contain events in $\text{EvUsed}'$, all distinguishers $D_0 \in \mathcal{D} \cup \{D_{\text{false}}\}$ that run in time at most $t_{D_0}$, all distinguishers $D_1$ that are disjunctions of events in $\mathcal{D}_{\text{SNU}}$,

$$ \begin{aligned} & \Pr[C[Q] : (D_0 \lor D_1 \lor D) \wedge \neg \text{NonUnique}_{Q,D_1 \lor D}] \\ & \le \Pr[C[Q'] : (D_0 \lor D_1 \lor D') \wedge \neg \text{NonUnique}_{Q',D_1 \lor D'}] + p(C, t_{D_0}) \end{aligned} \quad (1) $$

Intuitively, the events $\text{EvUsed}$ are those used by CryptoVerif in the sequence of games until the game $Q$ included, while the events $\text{EvUsed}'$ are those used until $Q'$. Hence, $\text{EvUsed}$ contains the events that occur in $Q$; $\text{EvUsed}'$ contains $\text{EvUsed}$ and the events that occur in $Q'$. The formula $D_0 \in \mathcal{D} \cup \{D_{\text{false}}\}$ corresponds to the initial query to prove: it is

* a correspondence distinguisher $\neg \varphi$ for a correspondence property (see Section 2.7.3);

* $S$ or $\neg \bar{S}$ for (one-session) secrecy (see Section 2.7.1) and bit secrecy (see Section 2.7.2);

* any distinguisher for indistinguishability;

* $D_{\text{false}}$ when the initial query has already been proved, and only Shoup and non-unique events remain to be proved.

We need to specify precisely the distinguishers needed for the queries we want to prove, because some game transformations of CryptoVerif rely on that. For instance, **simplify** (Section 5.1.21) removes events that are not used by the queries.

The formula $D_1$ is a disjunction of Shoup and non-unique events that remain to be proved, both in $Q$ and in $Q'$. These events are in $\mathcal{D}_{\text{SNU}}$ and in $\text{EvUsed}$. The formula $D$ is a disjunction of Shoup and non-unique events that remain to be proved in $Q$, while the formula $D'$ is a disjunction of Shoup and non-unique events that remain to be proved in $Q'$. Hence, the events that occur in $D$ and not in $D'$ are events proved while transforming $Q$ into $Q'$. ("Proving" an event means proving that this event has a negligible probability of occurring, and adding that probability to $p$.) In contrast, the events that occur in $D'$ and not in $D$ are fresh Shoup and non-unique events introduced during the transformation of $Q$ into $Q'$, and that will need to be proved later; hence these events are in $\text{EvUsed}'$ but not in $\text{EvUsed}$. More generally, all events that occur in $Q'$ but not in $Q$ are fresh events introduced in the transformation of $Q$ into $Q'$, so they are in $\text{EvUsed}'$ but not in $\text{EvUsed}$.
When there are no Shoup nor non-unique events, we have $D_1 = D = D' = D_{\text{false}}$ and $\text{NonUnique}_{Q,D_1 \lor D} = \text{NonUnique}_{Q',D_1 \lor D'} = D_{\text{false}}$, so the inequality (1) reduces to

$$ \Pr[C[Q] : D_0] \leq \Pr[C[Q'] : D_0] + p(C, t_{D_0}) $$

Using $\neg D_0$ instead of $D_0$, we obtain

$$ 1 - \Pr[C[Q] : D_0] \leq 1 - \Pr[C[Q'] : D_0] + p(C, t_{D_0}) $$

so by combining the two, $|\Pr[C[Q] : D_0] - \Pr[C[Q'] : D_0]| \leq p(C, t_{D_0})$ as in the definition of indistinguishability. In the general case, the inequality (1) differs from this formula because (1) always counts the traces that execute Shoup and non-unique events that remain to be proved (these traces are always included in the probability by $D_1 \lor D$, resp. $D_1 \lor D'$; the probability of these events needs to be bounded), and never counts the traces that execute proved non-unique events (these traces are excluded by $\neg \text{NonUnique}_{Q,D_1 \lor D}$, resp. $\neg \text{NonUnique}_{Q',D_1 \lor D'}$; the probability of these events has already been bounded). We could also exclude traces that execute proved Shoup events, though it is less essential: Shoup events often simply disappear when they are proved, while non-unique events remain in the game. Excluding traces that execute proved non-unique events allows us to exploit that the corresponding find or get is unique in the transformation from $Q$ to $Q'$: intuitively, the traces in which the find or get is not unique are not counted, so they can be ignored. (Obviously, this point needs to be proved more precisely for each game transformation.)

We need to introduce a distinct event for each $[\text{unique}_e]$ because not all $\text{find}[\text{unique}_e]$ and $\text{get}[\text{unique}_e]$ may be proved unique in the current process and because we need to distinguish the non-unique events that occur in $Q$ from those that occur in the context $C$. However, once a $[\text{unique}_e]$ is proved, its name does not matter: all such events are counted in $\text{NonUnique}_{Q,D_1 \lor D}$, and that remains true in future game transformations, since events are never re-added to $D_1$ or $D$. Therefore, we can rename all such events to the same name. So we simply abbreviate $[\text{unique}_e]$ by $[\text{unique}]$ when event $e$ is proved. The context $C$ must not contain the events used in $Q$ or $Q'$ and more generally events in $\text{EvUsed}'$.

The formula (1) could also be written

$$ \Pr[C[Q] : (D_0 \land \neg \text{NonUnique}_Q) \lor D_1 \lor D] \leq \Pr[C[Q'] : (D_0 \land \neg \text{NonUnique}_{Q'}) \lor D_1 \lor D'] + p(C, t_{D_0}) $$

since $\text{NonUnique}_{Q,D_1 \lor D} = \text{NonUnique}_Q \land \neg (D_1 \lor D)$. The advantage of the latter formulation is that the dependency in $D_1$, $D$, $D'$ is simpler, which we sometimes exploit in the proofs. However, its drawback is that it is less clear for which events the traces are always counted and for which ones they are never counted, because some events appear both in $\text{NonUnique}_Q$ and in $D_1 \lor D$. That is why we chose formula (1), to make it clear that the traces that execute events in $D_1 \lor D$ are always counted and the traces that execute events in $\text{NonUnique}_{Q,D_1 \lor D}$ are never counted.

When $f$ is a function from sequences of events to sequences of events and $D$ is a distinguisher, we define the distinguisher $D \circ f$ by $(D \circ f)(\mathcal{E}v) = D(f(\mathcal{E}v))$. In particular, when $\sigma$ is a renaming of events, the distinguisher $D \circ \sigma^{-1}$ is defined by $(D \circ \sigma^{-1})(\mathcal{E}v) = D(\sigma^{-1}\mathcal{E}v)$. When $D$ is defined as a logical formula, that corresponds to renaming the events in $D$. For instance, if $D = e_1 \lor \dots \lor e_m$, then $D \circ \sigma^{-1} = \sigma e_1 \lor \dots \lor \sigma e_m$. When $D$ is a set of distinguishers, $\sigma D = \{D \circ \sigma^{-1} | D \in D\}$.

We write $D_{\neg \mathcal{E}}$ for the set of distinguishers that do not use events in $\mathcal{E}$.

**Lemma 19** 1. Link with indistinguishability:
(a) Suppose that $\mathcal{D}_{\text{SNU}}$ is a set of Shoup events, $D$ is a distinguisher consisting of a disjunction of Shoup events, $Q, Q'$ do not contain non-unique events, the events that occur in $Q, D, D$, or $\mathcal{D}_{\text{SNU}}$ are in $\text{EvUsed}$, and the events that occur in $Q'$ also occur in $Q$. If $Q \approx_p^{V,\mathcal{E}} Q'$, then $D, \mathcal{D}_{\text{SNU}} : Q, D, \text{EvUsed} \xrightarrow{V} p Q', D, \text{EvUsed}$, for all $D, \mathcal{D}_{\text{SNU}}, D$ such that $\text{event}(D) \cap \text{EvUsed} \subseteq \mathcal{E}$, $\mathcal{D}_{\text{SNU}} \subseteq \mathcal{E}$, $\text{event}(D) \subseteq \mathcal{E}$.

(b) Suppose that $Q$ and $Q'$ do not contain non-unique events, the events that occur in $Q$ are in $\text{EvUsed}$, and the events that occur in $Q'$ also occur in $Q$. Then $\mathcal{D}_{-(\text{EvUsed}\setminus\mathcal{E})}, \emptyset : Q, D_{\text{false}}, \text{EvUsed} \xrightarrow{V} p Q', D_{\text{false}}, \text{EvUsed}$ if and only if $Q \approx_p^{V,\mathcal{E}} Q'$.

2. Reflexivity: If $\mathcal{D}_{\text{SNU}}$ is a set of Shoup and non-unique events in $\text{EvUsed}$, $D$ is a distinguisher consisting of a disjunction of Shoup and non-unique events, and the events that occur in $Q$ or in $D$ are in $\text{EvUsed}$, then $D, \mathcal{D}_{\text{SNU}} : Q, D, \text{EvUsed} \xrightarrow{V} _0 Q, D, \text{EvUsed}$.

3. Transitivity: If $\mathcal{D}, \mathcal{D}_{\text{SNU}} : Q, D, \text{EvUsed} \xrightarrow{V} _p Q', D', \text{EvUsed}'$ and $\mathcal{D}, \mathcal{D}_{\text{SNU}} : Q', D', \text{EvUsed}' \xrightarrow{V} _{p'} Q'', D'', \text{EvUsed}'$, then we have $\mathcal{D}, \mathcal{D}_{\text{SNU}} : Q, D, \text{EvUsed} \xrightarrow{V} _{p''} Q'', D'', \text{EvUsed}'$, where $p''(C, t_{D_0}) = p(C, t_{D_0}) + p'(C, t_{D_0})$.

4. Application of a context: If $\mathcal{D}_{-\text{EvUsed}'}$, $\mathcal{D}_{\text{SNU}} : Q, D, \text{EvUsed} \xrightarrow{V} _p Q', D', \text{EvUsed}'$, $\sigma$ is a renaming of the events in $\text{EvUsed}'$ to events not in $\text{EvUsed}^+$, $C$ is a context acceptable for $\sigma Q$ and $\sigma Q'$ with public variables $V$ such that $\text{event}(C) \subseteq \text{EvUsed}^+$, and $\mathcal{D}'_{\text{SNU}}$ is a set of Shoup and non-unique events in $\text{EvUsed}^+$, then we have $\mathcal{D}_{-\sigma\text{EvUsed}'}$, $\sigma\mathcal{D}_{\text{SNU}} \cup \mathcal{D}'_{\text{SNU}} : C[\sigma Q], D \circ \sigma^{-1}, \sigma\text{EvUsed} \cup \text{EvUsed}^+ \xrightarrow{V} _{p'} C[\sigma Q'], D' \circ \sigma^{-1}, \sigma\text{EvUsed}' \cup \text{EvUsed}^+$, where $p'(C', t_{D_0}) = p(\sigma^{-1}(C'[C]), t_{D_0})$, and $V' \subseteq V \cup \text{var}(C)$.

5. Adding distinguishers: If $\mathcal{D}, \mathcal{D}_{\text{SNU}} : Q, D, \text{EvUsed} \xrightarrow{V} _p Q', D', \text{EvUsed}'$ and $e \in \mathcal{D}_{\text{SNU}}$, then $\mathcal{D}, \mathcal{D}_{\text{SNU}} : Q, D \lor e, \text{EvUsed} \xrightarrow{V} _p Q', D' \lor e, \text{EvUsed}'$.

6. Removing distinguishers: If $\mathcal{D}, \mathcal{D}_{\text{SNU}} : Q, D, \text{EvUsed} \xrightarrow{V} _p Q', D', \text{EvUsed}'$, $\mathcal{D}' \subseteq \mathcal{D}$, and $\mathcal{D}'_{\text{SNU}} \subseteq \mathcal{D}_{\text{SNU}}$, then $\mathcal{D}', \mathcal{D}'_{\text{SNU}} : Q, D, \text{EvUsed} \xrightarrow{V} _p Q', D', \text{EvUsed}'$

**Proof** Property 1a: Given the hypothesis, $\mathcal{D}, \mathcal{D}_{\text{SNU}} : Q, D, \text{EvUsed} \xrightarrow{V} _p Q', D, \text{EvUsed}$ reduces to: for all evaluation contexts $C$ acceptable for $Q$ and $Q'$ with public variables $V$ that do not contain events in $\text{EvUsed}$, all distinguishers $D_0 \in \mathcal{D} \cup \{D_{\text{false}}\}$ that run in time at most $t_{D_0}$, and all distinguishers $D_1$ that are disjunctions of events in $\mathcal{D}_{\text{SNU}}$,

$$ \Pr[C[Q] : D_0 \lor D_1 \lor D] \leq \Pr[C[Q'] : D_0 \lor D_1 \lor D] + p(C, t_{D_0}) $$

We have $\text{event}(D_0 \lor D_1 \lor D) \cap \text{event}(Q, Q') \subseteq \text{event}(D_0 \lor D_1 \lor D) \cap \text{EvUsed} \subseteq \mathcal{E}$. Moreover, $D_0 \lor D_1 \lor D$ can be implemented in the same time as $D_0$ since evaluating $D_0 \lor D_1 \lor D$ can be done by setting the final result to true as soon as an event in $D_1 \lor D$ is executed, and evaluating $D_0$ otherwise. This does not take more time than evaluating $D_0$. So this inequality is a consequence of $Q \approx_p^{V,\mathcal{E}} Q'$.

Property 1b: Given the hypothesis, $\mathcal{D}_{-(\text{EvUsed}\setminus\mathcal{E})}, \emptyset : Q, D_{\text{false}}, \text{EvUsed} \xrightarrow{V} _p Q', D_{\text{false}}, \text{EvUsed}$ reduces to: for all evaluation contexts $C$ acceptable for $Q$ and $Q'$ with public variables $V$ that do not contain events in $\text{EvUsed}$, and all distinguishers $D_0 \in \mathcal{D}_{-(\text{EvUsed}\setminus\mathcal{E})}$ that run in time at most $t_{D_0}$,

$$ \Pr[C[Q] : D_0] \leq \Pr[C[Q'] : D_0] + p(C, t_{D_0}), $$