# Decidability of a Sound Set of Inference Rules for Computational Indistinguishability

Adrien Koutsos

► To cite this version:

Adrien Koutsos. Decidability of a Sound Set of Inference Rules for Computational Indistinguishability. 2019 IEEE 32nd Computer Security Foundations Symposium (CSF), Jun 2019, Hoboken, France. pp.48-4813, 10.1109/CSF.2019.00011. hal-04392610

HAL Id: hal-04392610

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

Submitted on 13 Jan 2024

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 Attribution 4.0 International License
# Decidability of a Sound Set of Inference Rules for Computational Indistinguishability

Adrien Koutsos

LSV, CNRS, ENS Paris-Saclay, Université Paris-Saclay

Cachan, France

adrien.koutsos@lsv.fr

**Abstract**—Computational indistinguishability is a key property in cryptography and verification of security protocols. Current tools for proving it rely on cryptographic game transformations.

We follow Bana and Comon’s approach [1], [2], axiomatizing what an adversary cannot distinguish. We prove the decidability of a set of first-order axioms which are computationally sound, though incomplete, for protocols with a bounded number of sessions whose security is based on an IND-CCA₂ encryption scheme. Alternatively, our result can be viewed as the decidability of a family of cryptographic game transformations. Our proof relies on term rewriting and automated deduction techniques.

***Index Terms***—Security Protocols, Automated Deduction, Decision Procedure, Computational Indistinguishability

## I. INTRODUCTION

Designing security protocols is notoriously hard. For example, the TLS protocol used to secure most of the Internet connections was successfully attacked several times at the protocol level, e.g. the LOGJAM attack [3] or the TRIPLEHANDSHAKE attack [4]. This shows that, even for high visibility protocols, and years after their design, attacks are still found.

Using formal methods to prove a security property is the best way to get a strong confidence. However, there is a difficulty, which is not present in standard program verification: we need not only to specify formally the program and the security property, but also the attacker. Several attacker models have been considered in the literature.

A popular attacker model, the *Dolev-Yao attacker*, grants the attacker the complete control of the network: he can intercept and re-route all messages. Besides, the adversary is allowed to modify messages using a fixed set of rules (e.g. given a cipher-text and its decryption key, he can retrieve the plaintext message). Formally, messages are terms in a term algebra and the rules are given through a set of rewrite rules. This model is very amenable to automatic verification of security properties. There are several automated tools, such as, e.g., ProVerif [5], Tamarin [6] and Deepsec [7].

Another attacker model, closer to a real world attacker, is the *computational attacker model*. This adversary also controls the network, but this model does not restrict the attacker to a fixed set of operations: the adversary can perform any probabilistic polynomial time computation. More formally, messages are bit-strings, random numbers are sampled uniformly among bit-strings in {0, 1}ⁿ (where n is the *security parameter*) and the attacker is any probabilistic polynomial-time Turing machine (PPTM). This model offers stronger guarantees than

the Dolev-Yao model (DY model), but formal proofs are harder to complete and more error-prone. There exist several formal verification tools in this model: for example, EASYCRYPT [8] which relies on pRHL, and CRYPTOVERIF [9] which performs game transformations. As expected, such tools are less automatic than the verification tools in the DY model. Moreover, the failure to find a proof in such tools, either because the proof search failed or did not terminate, or because the user could not manually find a proof, does not give any indication on the actual security of the protocol.

There is an alternative approach, the Bana-Comon model (BC model), introduced in [2]. In this model, we express the security of a protocol as the unsatisfiability of a set of formulas in first-order logic. The formulas contain the negation of the security property and *axioms*, which reflect implementation assumptions, such as functional correctness and cryptographic hypotheses on the security primitives. This method has several advantages over pRHL and game transformations. First, it is simpler, as there is no security game and no probabilities, only a first-order formula. Then, carrying out a proof of unsatisfiability in this logic entails the security of the protocol in the computational model. Finally, the absence of such a proof implies the existence of a model of the formula, i.e. an attack, albeit not necessarily a computational one; nonetheless, we know that the security of the protocol *cannot* be obtained without extra assumptions. Note that the Bana-Comon approach is only valid for protocols with a finite number of sessions (there is no unbounded replication). Since this is the model we use, we inherit this restriction.

There is another input to security proofs that we did not discuss yet: the class of security properties considered. Roughly, there are two categories. *Reachability properties* state that some bad state is unreachable. This includes, for example, authentication or (weak) secrecy. *Indistinguishability properties* state that an adversary cannot distinguish between the executions of two protocols. This allows for more complex properties, such as strong secrecy and unlinkability.

a) *Deciding Security:* When trying to prove a protocol, there are three possible outcomes: either we find a proof, which gives security guarantees corresponding to the attacker model; or we find an attack, meaning that the protocol is insecure; or the tool or the user (for interactive provers) could not carry out the proof and failed to find an attack. The latter case may happen for two different reasons. First, we could
neither find a proof nor an attack because the proof method used is incomplete. In that case, we need either to make new assumptions and try again, or to use another proof technique. Second, the tool may not terminate on the protocol considered. This is problematic, as we do not know if we should continue waiting, and consume more resources and memory, or try another method.

This can be avoided for decidable classes of protocols and properties. Of course, such classes depend on both the attacker model and the security properties considered. We give here a non-exhaustive survey of such results. In the symbolic model, [10] shows decidability of secrecy (a reachability property) for a bounded number of sessions. In [11], the authors show the decidability of a secrecy property for depth-bounded protocols, with an unbounded number of sessions, using Well-Structured Transition Systems [12]. Chrétien et al [13] show the decidability of indistinguishability properties for a restricted class of protocols. E.g., they consider processes communicating on distinct channels and without else branches. The authors of [14] show the decidability of symbolic equivalence for a bounded number of sessions, but with conditional branching.

In the computational model, we are aware of only one direct result. In [15], the authors show the decidability of the security of a formula in the BC model, for reachability properties, for a bounded number of sessions. But there is an indirect way of getting decidability in the computational model, through a computational soundness theorem (e.g. [16]). A computational soundness theorem states that, for some given classes of protocols and properties, symbolic security implies computational security. These results usually make strong implementation assumptions (e.g. parsing assumptions, or the absence of dishonest keys), and require that the security primitives satisfy strong cryptographic hypothesis. By combining a decidability result in the symbolic model with a computational soundness theorem, which applies to the considered classes of protocols and properties (e.g. [17] for reachability properties, or [18] for indistinguishability properties), we obtain a decidability result in the computational model.

We discuss further related works later, in Section VIII.

b) Contributions: In this paper, we consider the BC model for indistinguishability properties [1]. This is a first-order logic in which we design a set of axioms Ax which includes, in particular, axioms for the IND-CCA₂ cryptographic assumption [19]. Given a protocol and a security property, we can build, using a folding technique described in [1], a ground atomic formula $\psi$ expressing the security of the protocol. Showing the unsatisfiability of the conjunction of the axioms Ax and the negation of $\psi$ entails the security of the protocol in the computational model, assuming that the encryption scheme is IND-CCA₂ secure.

Our main result is the decidability of the problem:

**Input:** A ground formula $\vec{u} \sim \vec{v}$.

**Question:** Is $Ax \wedge \vec{u} \not\sim \vec{v}$ unsatisfiable?

That is, we show the decidability of a sound, though incomplete, axiomatization of computational indistinguishability.

All the formulas in Ax are Horn clauses, therefore to show the unsatisfiability of $Ax \wedge \vec{u} \not\sim \vec{v}$ we use resolution with a negative strategy: we see axioms in Ax as inference rules and look for a derivation of the goal $\vec{u} \sim \vec{v}$. We prove the decidability of the corresponding satisfiability problem.

The main difficulty lies in dealing with equalities (defined through a term rewriting system $R$). First we show the completeness of an ordered strategy by commuting rule applications. This allows us to have only one rewriting modulo $R$ at the beginning of the proof. We then bound the size of the terms after this rewriting as follows: we identify a class of proof cuts introducing arbitrary subterms; we give proof cut eliminations to remove them; and finally, we show that cut-free proofs are of bounded size w.r.t. the size of the conclusion.

c) Game Transformations: Our result can be reinterpreted as the decidability of the problem of determining whether there exits a sequence of game transformations [20], [21] that allows to prove the security of a protocol. Indeed, one can associate to every axiom in Ax either a cryptographic assumption or a game transformation.

Each unitary axiom in Ax (an atomic formula) corresponds to an instantiation of the IND-CCA₂ game. For instance, in the simpler case of IND-CPA security of an encryption $\{\_\}_{pk}^n$, no polynomial-time adversary can distinguish between two cipher-texts, even if it chooses the two corresponding plain-texts (here, $n$ is the explicit encryption randomness). Initially, the public key pk is given to the adversary, who computes a pair of plain-texts $g(pk)$: $g$ is interpreted as the adversary's computation. Then the two cipher-texts, corresponding to the encryptions of the first and second components of $g(pk)$, should be indistinguishable. This yields the unitary axiom:

$$ \{\pi_1(g(pk))\}_{pk}^n \sim \{\pi_2(g(pk))\}_{pk}^n $$

Similarly, non-unitary axioms correspond to cryptographic game transformations. E.g., the function application axiom:

$$ \vec{u} \sim \vec{v} \rightarrow f(\vec{u}) \sim f(\vec{v}) $$

states that if no adversary can distinguish between the arguments of a function call, then no adversary can distinguish between the images. As for a cryptographic game transformation, the soundness of this axiom is shown by reduction. Given a winning adversary $A$ against the conclusion $f(\vec{u}) \sim f(\vec{v})$, we build a winning adversary $B$ against $\vec{u} \sim \vec{v}$: the adversary $B$, on input $\vec{w}$ (which was sampled from $\vec{u}$ or $\vec{v}$), computes $f(\vec{w})$ and then gives the result to the distinguisher $A$. The advantage of $B$ against $\vec{u} \sim \vec{v}$ is then the advantage of $A$ against $f(\vec{u}) \sim f(\vec{v})$, which is (by hypothesis) non negligible.

By interpreting every axiom in Ax as a cryptographic assumption or a game transformation, and the goal formula $\vec{u} \sim \vec{v}$ as the initial game, our result can be reformulated as showing the decidability of the following problem:

**Input:** An initial game $\vec{u} \sim \vec{v}$.

**Question:** Is there a sequence of game transformations in Ax showing that $\vec{u} \sim \vec{v}$ is secure?
and random tapes $\rho_1, \rho_2, M$ returns 1 if $M_1(w, \rho_1, \rho_2) = M_2(w, \rho_1, \rho_2)$ and 0 otherwise. The function symbol $\mathbf{0}$ is interpreted as the function that, on input of length $l$, returns the bit-string $0^l$.

* A function symbol $g \in \mathcal{G}$ with $n$ arguments is interpreted as a function $[[g]]$ such that there is a polynomial-time Turing machine $M_g$ such that for every machines $(m_i)_{i \le n}$ in the interpretation domains, and for every inputs $w, \rho_1, \rho_2$:

$$[[g]]((m_i)_{i \le n})(w, \rho_1, \rho_2) = M_g((m_i(w, \rho_1, \rho_2))_{i \le n}, \rho_2)$$

Observe that $M_g$ cannot access directly the tape $\rho_1$.

* Protocol function symbols are interpreted as deterministic polynomial-time Turing machine. Their interpretations will be restricted using implementation axioms later.

* The interpretation of function symbols is lifted to terms: given an assignment $\sigma$ of the variables of a term $t$ to elements of the appropriate domains, we write $[[t]]_{\eta, \rho_1, \rho_2}^{\sigma}$ the interpretation of the term with respect to $\eta, \rho_1, \rho_2$. $\sigma$ is omitted when empty. We also omit the other parameters when they are irrelevant.

* The predicate $\sim_n$ is interpreted as computational indistinguishability $\approx$, defined by $m_1, \dots, m_n \approx m'_1, \dots, m'_n$ iff for every PPTM $\mathcal{A}$ with random tape $\rho_2$:

$$| \Pr(\rho_1, \rho_2 : \mathcal{A}((m_i(1^\eta, \rho_1, \rho_2))_{1 \le i \le n}, \rho_2) = 1) - \\ \Pr(\rho_1, \rho_2 : \mathcal{A}((m'_i(1^\eta, \rho_1, \rho_2))_{1 \le i \le n}, \rho_2) = 1) |$$

is negligible in $\eta$ (a function is negligible if it is asymptotically smaller than the inverse of any polynomial). Moreover, for all ground terms $u, v$, we write $M_c \models u \sim v$ when $[[u]] \approx [[v]]$ in $M_c$.

**Example 1.** Let $n_0, n_1, n \in \mathcal{N}$ and $g \in \mathcal{F}$ of arity zero. For every computational model $M_c$:

$$M_c \models \text{if } g() \text{ then } n_0 \text{ else } n_1 \sim n$$

Indeed, the term on the left represents the message obtained by letting the adversary choose a branch, and then sampling from $n_0$ or $n_1$ accordingly. This is semantically equivalent to directly performing a random sampling, as done on the right.

### III. AXIOMS

We present the axioms $Ax$, which are of two kinds:

* structural axioms represent properties that hold in every computational model. This includes axioms such as the symmetry of $\sim$, or properties of the `ifThenElse_`.

* implementation axioms reflect implementation assumptions, such as the functional correctness of the pair and projections (e.g. $\pi_1(\langle u, v \rangle) = u$), or cryptographic assumptions on the security primitives (e.g. `IND-CCA2`).

All our axioms $Ax$ are universally quantified Horn clauses. To show the unsatisfiability of $Ax \wedge \vec{u} \not\sim \vec{v}$, we use resolution with a negative strategy (which is complete, see [26]). As all axioms are Horn clauses, a proof by resolution with a negative strategy can be seen as a proof tree where each node is indexed by the axiom of $Ax$ used at this resolution step. Hence, axioms will be given as inference rules (where variables are implicitly universally quantified).

### A. Equality and Structural Axioms

Some notation conventions: we use $\vec{u}$ to denote a vector of terms; and we use an infix notation for $\sim$, writing $\vec{u} \sim \vec{v}$ when $\vec{u}$ and $\vec{v}$ are of the same length.

The equality and structural axioms we present here already appeared in the literature [1], [22], [27], sometimes with slightly different formulations.

**a) Equality:** Computational indistinguishability is an equivalence relation (i.e. reflexive, symmetric and transitive). But we can observe that it is not a congruence. E.g. take a computational model $M_c$, we know that two names $n$ and $n'$ are indistinguishable (since they are interpreted as independent uniform random sampling in $\{0, 1\}^\eta$), and $n$ is indistinguishable from itself. Therefore:

$$M_c \models n \sim n' \quad \text{and} \quad M_c \models n \sim n$$

But there is a simple PPTM that can distinguish between $\langle n, n \rangle$ and $\langle n', n \rangle$: simply test whether the two arguments are equal, if so return 1 and otherwise return 0. Then, with overwhelming probability, this machine will guess from which distribution its input was sampled from.

Even though $\sim$ is not a congruence, we can get a congruence from it: if $\text{eq}(s, t) \sim \text{true}$ holds in all models then, using the semantics of $\text{eq}(\_, \_)$, in every computational model $M_c$, $[[s]]$ and $[[t]]$ are identical except for a negligible number of samplings. Hence we can replace any occurrence of $s$ by $t$ in a formula without changing its semantics with respect to computational indistinguishability.

We use this in our logic as follows: we let $s = t$ be a shorthand for $\text{eq}(s, t) \sim \text{true}$, and we introduce a set of equalities $R$ (given in Fig. 1) and its congruence closure $=_{R}$. We split $R$ in four sub-parts: $R_1$ contains the functional correctness assumptions on the pair and encryption; $R_2$ and $R_3$ contain, respectively, the homomorphism properties and simplification rules of the `ifThenElse_`; and $R_4$ allows to change the order in which conditional tests are performed.

We then introduce a recursive set of rules:

$$\frac{\vec{u}, t \sim \vec{v}}{\vec{u}, s \sim \vec{v}} R \quad (s, t \text{ ground terms with } s =_R t)$$

By orienting $R_1, R_2, R_3$ from left to right, and carefully choosing an orientation for the ground instances of $R_4$, we obtain a recursive term rewriting system $\rightarrow_R$. We have the following theorem (the proof is in the long version [25]):

**Theorem 1.** The TRS $\rightarrow_R$ is convergent on ground terms.

**b) Structural Axioms:** We now give an informal description of the axioms given in Fig. 2. We describe in details the case study axiom CS, which is the most complicated one. It states that in order to show that:

$$\text{if } b \text{ then } u \text{ else } v \sim \text{if } b' \text{ then } u' \text{ else } v'$$

it is sufficient to show that the `then` branches and the `else` branches are indistinguishable, when giving to the adversary the value of the conditional (i.e. $b$ on the left and $b'$ on the right). We can do better, by considering simultaneously several
$$
\begin{align*}
R_1 \quad \left\{
\begin{array}{@{}l@{}}
\pi_i(\langle x_1, x_2 \rangle) = x_i \quad \text{eq}(x, x) = \text{true} \\
\text{dec}(\{x\}_{\text{pk}(y)}^z, \text{sk}(y)) = x
\end{array}
\right. & \\
R_2 \quad \left\{
\begin{array}{@{}l@{}}
f(\vec{u}, \text{if } b \text{ then } x \text{ else } y, \vec{v}) = \\
\quad \text{if } b \text{ then } f(\vec{u}, x, \vec{v}) \text{ else } f(\vec{u}, y, \vec{v}) \quad (f \in \mathcal{F}_s) \\
\text{if } (\text{if } b \text{ then } a \text{ else } c) \text{ then } x \text{ else } y = \\
\quad \text{if } b \text{ then } (\text{if } a \text{ then } x \text{ else } y) \text{ else } (\text{if } c \text{ then } x \text{ else } y)
\end{array}
\right. & \\
R_3 \quad \left\{
\begin{array}{@{}l@{}}
\text{if } b \text{ then } x \text{ else } x = x \\
\text{if true then } x \text{ else } y = x \quad \text{if false then } x \text{ else } y = y \\
\text{if } b \text{ then } (\text{if } b \text{ then } x \text{ else } y) \text{ else } z = \text{if } b \text{ then } x \text{ else } z \\
\text{if } b \text{ then } x \text{ else } (\text{if } b \text{ then } y \text{ else } z) = \text{if } b \text{ then } x \text{ else } z
\end{array}
\right. & \\
R_4 \quad \left\{
\begin{array}{@{}l@{}}
\text{if } b \text{ then } (\text{if } a \text{ then } x \text{ else } y) \text{ else } z = \\
\quad \text{if } a \text{ then } (\text{if } b \text{ then } x \text{ else } z) \text{ else } (\text{if } b \text{ then } y \text{ else } z) \\
\text{if } b \text{ then } x \text{ else } (\text{if } a \text{ then } y \text{ else } z) = \\
\quad \text{if } a \text{ then } (\text{if } b \text{ then } x \text{ else } y) \text{ else } (\text{if } b \text{ then } x \text{ else } z)
\end{array}
\right.
\end{align*}
$$

<caption>Fig. 1. $R = R_1 \cup R_2 \cup R_3 \cup R_4$</caption>

terms starting with the same conditional. We also allow some
terms $\vec{w}$ and $\vec{w}'$ on the left and right to stay untouched:

$$
\frac{\vec{w}, b, (u_i)_i \sim \vec{w}', b', (u'_i)_i \qquad \vec{w}, b, (v_i)_i \sim \vec{w}', b', (v'_i)_i}{\vec{w}, (\text{if } b \text{ then } u_i \text{ else } v_i)_i \sim \vec{w}', (\text{if } b' \text{ then } u'_i \text{ else } v'_i)_i}
$$

This is the only axiom with more than one premise. Further-
more we assume that b, b' do not contain conditionals.

We quickly describe the other structural axioms: Perm allows to change the terms order, using the same permutation on both sides of ~; Restr is a strengthening axiom; R allows to replace a term s by any R-equal term t; the function application axiom FA states that to prove that two images are indistinguishable, it is sufficient to show that the arguments are indistinguishable (we restrict this axiom to the case where f is in $\mathcal{F} \setminus \{0\}$); Sym states that indistinguishability is symmetrical; and Dup states that giving twice the same value to an adversary is equivalent to giving it only once. All the above axioms are computationally valid.

**Proposition 1.** The axioms given in Fig. 2 are valid in any computational model in which the functional correctness assumptions $R_1$ on pairs and encryptions hold.

Proof. The proof can be found in [1].

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

c) **Restrictions:** As mentioned earlier, we restricted some axioms to achieve decidability. For example, the CS and FA axioms presented above are weaker than the corresponding axioms in [1]: in the CS axiom, we forbid the terms $b$ and $b'$ from containing conditionals; and we do not allow FA applications on the **0** function symbols. These are technical restrictions which are used in the proof, but might be unnecessary.

B. Cryptographic Assumptions

We now show how cryptographic assumptions are translated
into unitary axioms. In the computational model, the security
of a cryptographic primitive is expressed through a game
between a challenger and an attacker (which is a PPTM) that
tries to break the primitive.

We present here the IND-CCA₂ game (for Indistinguishabil-
ity against Chosen Ciphertexts Attacks, see [19]). First, the

challenger computes a public/private key pair (pk(n), sk(n))
(using a nonce n of length η uniformly sampled), and sends
pk(n) to the attacker. The adversary then has access to two
oracles: i) a left-right oracle O<sup>b</sup><sub>LR</sub>(n) that takes two messages
m<sub>0</sub>, m<sub>1</sub> as input and returns {m<sub>b</sub>}<sup>n<sub>r</sub></sup><sub>pk(n)</sub>, where b is an internal
bit uniformly sampled at the beginning by the challenger and
n<sub>r</sub> is a fresh nonce; ii) a decryption oracle O<sub>dec</sub>(n) that, given
m, returns dec(m, sk(n)) if m was not the result of a previous
O<sub>LR</sub> oracle query, and length of m zeros otherwise. Remark
that the two oracles have a shared memory. For simplicity,
we omit the length constraints of these oracles (they can be
found the long version [25]) The advantage Adv<sup>CCA2</sup><sub>A</sub>(η) of
an adversary A against this game is the probability for A to
guess the bit b:

$$
\left| \Pr(\mathbf{n} : \mathcal{A}^{\mathcal{O}_{\text{LR}}^{1}(\mathbf{n}), \mathcal{O}_{\text{dec}}(\mathbf{n})}(1^{\eta}) = 1) - \Pr(\mathbf{n} : \mathcal{A}^{\mathcal{O}_{\text{LR}}^{0}(\mathbf{n}), \mathcal{O}_{\text{dec}}(\mathbf{n})}(1^{\eta}) = 1) \right|
$$

An encryption scheme is IND-CCA<sub>2</sub> if the advantage
Adv<sub>A</sub><sup>CCA2</sup>(η) of any adversary A is negligible in η. The
IND-CCA<sub>1</sub> game is the restriction of this game where the
adversary cannot call O<sub>dec</sub> after having called O<sub>LR</sub>. An
encryption scheme is IND-CCA<sub>1</sub> if Adv<sub>A</sub><sup>CCA1</sup>(η) is negligible
for any adversary A.

a) **CCA1 Axiom:** Before introducing the CCA2 axioms, we recall informally the CCA1 axioms from [1]. First, we define a syntactic property on secret keys used as a side-condition of the CCA1 axioms:

**Definition 1.** For every ground term *t*, we say that a secret key *sk*(*n*) appears only in decryption position in *t* if it appears only in subterms of *t* of the form *dec*(*_, sk*(*n*)).

We now define the CCA1 axioms:

**Definition 2.** CCA1 is the computable set of unitary axioms:

$$
\vec{w}, t[\{u\}_{\text{pk}(n)}^{n_r}] \sim \vec{w}, t[\{v\}_{\text{pk}(n)}^{n_r}]
$$

where: $n_r$ does not appear in $t, u, v, \vec{w}$; $\mathbf{n}$ appears only in $\mathbf{pk}(n)$ or $\mathbf{sk}(n)$ in $t, u, v, \vec{w}$; $\mathbf{sk}(n)$ does not appear in $t, \vec{w}$; $\mathbf{sk}(n)$ appears only in decryption position in $u, v$; and the terms $u$ and $v$ are always of the same length.

**Proposition 2.** CCA1 is valid in every computational model where the encryption scheme interpretation is IND-CCA₁.

*Proof.* (sketch) The proof is a reduction that, given a PPTM $\mathcal{A}$ that can distinguish between $\vec{w}, t[\{u\}_{\text{pk}(n)}^{n_r}]$ and $\vec{w}, t[\{v\}_{\text{pk}(n)}^{n_r}]$, builds a winning adversary against the IND-CCA<sub>1</sub> game.

We define the adversary. First, it computes [[u]] and [[v]]
calling the decryption oracle if necessary. It then sends them
to the challenger who answers c, which is either [[{u}]<sup>n<sub>r</sub></sup><sub>pk(n)</sub>] or
[[{v}]<sup>n<sub>r</sub></sup><sub>pk(n)</sub>]. Observe that we need the freshness hypothesis on
n<sub>r</sub> as it is drawn by the challenger and the adversary cannot
sample it. Using c, the adversary computes [[t[c]]], which it can
do because the secret key does not appear in t, and then returns
the bit A([[(t[c])]]). The advantage of the adversary is exactly the
advantage of A, which we assumed non-negligible, hence the
adversary wins the game.

<figure><img src="image_3.png" /></figure>
$$
\frac{u_{\pi(1)}, \dots, u_{\pi(n)} \sim v_{\pi(1)}, \dots, v_{\pi(n)}}{u_1, \dots, u_n \sim v_1, \dots, v_n} \text{Perm} \qquad \frac{\vec{u}, t \sim \vec{v}, t'}{\vec{u} \sim \vec{v}} \text{Restr} \qquad \text{for any } s=R \text{t, } \frac{\vec{u}, t \sim \vec{v}}{\vec{u}, s \sim \vec{v}} R \qquad \frac{\vec{u}_1, \vec{v}_1 \sim \vec{u}_2, \vec{v}_2}{f(\vec{u}_1), \vec{v}_1 \sim f(\vec{u}_2), \vec{v}_2} \text{FA} \\
\frac{\vec{u}, t \sim \vec{v}, t'}{\vec{u}, t, t \sim \vec{v}, t', t'} \text{Dup} \qquad \frac{\vec{v} \sim \vec{u}}{\vec{u} \sim \vec{v}} \text{Sym} \qquad \text{for any } b, b' \in \mathcal{T}(\mathcal{F}_s, \mathcal{N}), \frac{\vec{w}, b, (u_i)_i \sim \vec{w}', b', (u'_i)_i}{\vec{w}, (\text{if } b \text{ then } u_i \text{ else } v_i)_i \sim \vec{w}', (\text{if } b' \text{ then } u'_i \text{ else } v'_i)_i} \text{CS}
$$

**Conventions:** $\pi$ is a permutation of $\{1, \dots, n\}$ and $f \in \mathcal{F} \setminus \{0\}$.

<caption>Fig. 2. The Axioms Struct-Ax.</caption>

**Remark 1.** In the CCA1 axiom, we did not specify how we ensure that $u$ and $v$ are always of the same length. Since the length of a term depends on implementation details (e.g. how the pair $\langle_, \rangle$ implemented), we let the user supply implementation assumptions, but require that these assumptions satisfy some properties (this is necessary to get decidability). To simplify the presentation, we omit all length constraints in the rest of this paper. We explain how they are handled in the long version [25].

b) CCA2 Axiom: To extend this axiom to the IND-CCA₂ game, we need to deal with calls to the decryption oracle performed after some calls to the left-right oracle. For example, consider the case where one call $(u, v)$ was made. Let $\alpha = \{u\}_{\text{pk}(n)}^{n_r}$ and $\alpha' = \{v\}_{\text{pk}(n)}^{n_r}$ (where $\equiv$ denotes syntactic equality) be the result of the call on, respectively, the left and the right. A naive first try could be to state that decryptions are indistinguishable. That is, if we let $s \equiv t[\alpha]$ and $s' \equiv t[\alpha']$, then $\text{dec}(s, \text{sk}(n)) \sim \text{dec}(s', \text{sk}(n))$. But this is not valid: for example, take $u \equiv 0, v \equiv 1, t \equiv g(\emptyset)$ (where $\emptyset$ is a hole variable). Then the adversary can, by interpreting $g$ as the identity function, obtain a term semantically equal to 0 on the left and 1 on the right. This allows him to distinguish between the left and right cases.

We prevent this by adding a guard checking that we are not decrypting $\alpha$ on the left (resp. $\alpha'$ on the right): if not, we return the decryption $\text{dec}(s, \text{sk}(n))$ (resp. $\text{dec}(s', \text{sk}(n))$) asked for, otherwise we return a dummy message $\mathbf{0}(\text{dec}(s, \text{sk}(n)))$ (resp. $\mathbf{0}(\text{dec}(s', \text{sk}(n)))$).

**Definition 3.** CCA² is the (recursive) set of unitary axioms:

$$
\begin{array}{l}
\vec{w}, t[\alpha], \text{ if } eq(s, \alpha) \text{ then } \mathbf{0}(\text{dec}(t[\alpha], sk(n))) \\
\phantom{\vec{w}, t[\alpha], \text{ if }} \text{else } \text{dec}(t[\alpha], sk(n)) \\
\sim \vec{w}, t[\alpha'], \text{ if } eq(s', \alpha') \text{ then } \mathbf{0}(\text{dec}(t[\alpha'], sk(n))) \\
\phantom{\sim \vec{w}, t[\alpha'], \text{ if }} \text{else } \text{dec}(t[\alpha'], sk(n))
\end{array}
$$

under the side-conditions of Definition 2.

This axiom is valid whenever the encryption is IND-CCA₂.

**Proposition 3.** CCA² is valid in every computational model where the encryption scheme interpretation is IND-CCA₂.

This construction can be generalized to any number of calls to the left-right oracle, by adding a guard for each call, and to any number of keys. The general CCA2 axioms can be found

in the long version [25].<fnref n="1" /> Still, a few comments: we use extra syntactic side-conditions to remove superfluous guards; we allow for $\alpha$-renaming of names; we restrict $t$ to be without if-then-else and $0$; the axioms allow for an arbitrary number of public/private key pairs to be used simultaneously; and finally, an instance of the axiom can contain any number of interleaved left-right and decryption oracles calls.

**Remark 2.** The last point is what allows us to avoid transitivity in proofs. For example, consider four encryptions, two of them ($\alpha$ and $\gamma$) using the public key pk(n), and the other two ($\beta$ and $\delta$) using the public key pk(n'):

$$
\alpha \equiv \{A\}_{\text{pk}(n)}^{n_0} \quad \beta \equiv \{B\}_{\text{pk}(n')}^{n_1} \quad \gamma \equiv \{C\}_{\text{pk}(n)}^{n_0} \quad \delta \equiv \{D\}_{\text{pk}(n')}^{n_1}
$$

Then the following formula is a valid instance of the CCA2 axioms on, simultaneously, keys pk(n) and pk(n'):

$$
\overline{\alpha, \beta \sim \gamma, \delta} \quad \text{CCA2}(\text{pk}(n), \text{pk}(n'))
$$

However, proving the above formula using CCA2 only on one key at a time, as in [1], requires transitivity:

$$
\frac{\overline{\alpha, \beta \sim \alpha, \delta} \quad \text{CCA2}(\text{pk}(n'))}{\alpha, \beta \sim \gamma, \delta} \quad \overline{\alpha, \delta \sim \gamma, \delta} \quad \text{CCA2}(\text{pk}(n))
$$

### C. Comments and Examples

Our set of axioms is not complete w.r.t. the computational interpretation semantics. Indeed, being so would mean axiomatizing exactly which distributions (computable in polynomial time) can be distinguished by PPTMs, which is unrealistic and would lead to undecidability. E.g., if we completely axiomatized IND-CCA₂, then showing the satisfiability of our set of axioms would show the existence of IND-CCA₂ functions, which is an open problem.

Still, our axioms are expressive enough to complete concrete proofs of security. We illustrate this with two simple examples: a proof of the formula in Example 1, and a proof of the security of one round of the NSL protocol [28]. Of course, such proofs can be found automatically using our decision procedure.

**Example 2.** We give a proof of the formula of Example 1:

$$
\text{if } g() \text{ then } n_0 \text{ else } n_1 \sim n
$$

First, we introduce a conditional $g()$ on the right to match the structure of the left side using $R$. Then, we split the proof

<footnote n="1">¹Note that axioms for the IND-CCA₂ cryptographic assumption have already appeared in the literature, in [27]. These axioms are only for a single call to the left-right oracle, and a single key. Our axiom schema is more general.</footnote>
in two using the CS axiom. We conclude using the reflexivity modulo α-renaming axiom (this axiom is subsumed by CCA2, therefore we do not include it in AX).

$$ \frac{\begin{array}{c} g(), n_0 \sim g(), n \\ \text{REFL} \\ \text{CS} \\ R \end{array}}{\begin{array}{c} \text{if } g() \text{ then } n_0 \text{ else } n_1 \sim \text{if } g() \text{ then } n \text{ else } n \\ \text{if } g() \text{ then } n_0 \text{ else } n_1 \sim n \end{array}} $$

a) Proof of NSL: We consider a simple setting with one initiator A, one responder B and no key server. An execution of the NSL protocol is given in Fig. 3.

We write this in the logic. First, we let $pk_A \equiv pk(n_A)$ and $sk_A \equiv sk(n_A)$ be the public/private key pair of agent A (we define similarly ($pk_B, sk_B$)). Since A does not wait for any input before sending its first message, we put it into the initial frame:

<figure><img src="image_4.png" /><figcaption>Fig. 3. The NSL protocol.</figcaption></figure>

$$ \phi_0 \equiv \mathbf{pk}_A, \mathbf{pk}_B, \{\langle n_A, A \rangle\}_{\mathbf{pk}_B}^{n_0} $$

Then, both agents wait for a message before sending a single reply. When receiving $\mathbf{x}_A$ (resp. $\mathbf{x}_B$), the answer of agent A (resp. B) is expressed in the logic as follows:

$$ \begin{array}{l} t_A[\mathbf{x}_A] \equiv \text{if } \mathbf{eq}(\pi_1(\mathbf{dec}(\mathbf{x}_A, \mathbf{sk}_A)), n_A) \quad \text{then} \\ \text{if } \mathbf{eq}(\pi_2(\pi_2(\mathbf{dec}(\mathbf{x}_A, \mathbf{sk}_A))), B) \text{ then} \\ \quad \{\pi_1(\pi_2(\mathbf{dec}(\mathbf{x}_A, \mathbf{sk}_A)))\}_{\mathbf{pk}_B}^{n_2} \end{array} $$

$$ t_B[\mathbf{x}_B] \equiv \text{if } \mathbf{eq}(\pi_2(\mathbf{dec}(\mathbf{x}_B, \mathbf{sk}_B)), A) \quad \text{then} \\ \quad \{\langle \pi_1(\mathbf{dec}(\mathbf{x}_B, \mathbf{sk}_B)), \langle n_B, B \rangle \rangle\}_{\mathbf{pk}_A}^{n_1} $$

During an execution of the protocol, the adversary has several choices. First, it decides whether to interact first with A or B. We focus on the case where it first sends a message to B (the other case is similar). Then, it can honestly forward the messages or forge new ones. E.g., when sending the first message to B, it can either forward A's message $\{\langle n_A, A \rangle\}_{\mathbf{pk}_B}^{n_0}$ or forge a new message. We are going to prove the security of the protocol in the following case (the other cases are similar):

* the first message, sent to B, is honest. Therefore we take $\mathbf{x}_B \equiv \{\langle n_A, A \rangle\}_{\mathbf{pk}_B}^{n_0}$, and the answer from B is:

$$ t_B[\mathbf{x}_B] =_R \{\langle n_A, \langle n_B, B \rangle \rangle\}_{\mathbf{pk}_A}^{n_1} $$

* the second message, sent to A, is forged. Therefore we take $\mathbf{x}_A \equiv g(\phi_1)$, where $\phi_1 \equiv \phi_0, t_B[\mathbf{x}_B]$. As, a priori, nothing prevents $g(\phi_1)$ from being equal to $t_B[\mathbf{x}_B]$, we use the conditional $\mathbf{eq}(g(\phi_1), t_B[\mathbf{x}_B])$ to ensure that this message is forged. The answer from A is then:

$$ s \equiv \mathbf{if} \ \mathbf{eq}(g(\phi_1), t_B[\mathbf{x}_B]) \ \mathbf{then} \ 0 \ \mathbf{else} \ t_A[g(\phi_1)] \quad (1) $$

We show the secrecy of the nonce $n_B$: we let $t'_B[\mathbf{x}_B]$ (resp. $s'$) be the term $t_B[\mathbf{x}_B]$ (resp. $s$) where we replaced all occurrences

of $n_B$ by 0. For example, $t'_B[\mathbf{x}_B] =_R \{\langle n_A, \langle 0, B \rangle \rangle\}_{\mathbf{pk}_A}^{n_1}$. This yields the following goal formula:

$$ \phi_0, t_B[\mathbf{x}_B], s \sim \phi_0, t'_B[\mathbf{x}_B], s' \quad (2) $$

Remark 3. The process of computing the formula from the protocol description can be done automatically, using a simple procedure similar to the folding procedure from [1]. The formula in (2) has already been split between the honest and dishonest cases using the case study axiom CS (we omit the CS applications to keep the proof readable). For example, the term in (1) is the “else” branch of a CS application on conditional $\mathbf{eq}(g(\phi_1), t_B[\mathbf{x}_B])$ (which does not contain nested conditionals, as required by the CS side-condition).

We now proceed with the proof. We let $\delta$ be the guarded decryption that will be used in the CCA2 axiom:

$$ \delta \equiv \mathbf{if} \ \mathbf{eq}(g(\phi_1), t_B[\mathbf{x}_B]) \ \mathbf{then} \ 0(\mathbf{dec}(g(\phi_1), \mathbf{sk}_A)) \quad (3) \\ \mathbf{else} \ \mathbf{dec}(g(\phi_1), \mathbf{sk}_A) $$

and $s_\delta$ be the term $s$ where all occurrences of $\mathbf{dec}(g(\phi_1), \mathbf{sk}_A)$ have been replaced by $\delta$. We have $s =_R s_\delta$. We also introduce shorthands for some subterms of $s_\delta$: we let $a_\delta, b_\delta$ and $e_\delta$ be the terms $\mathbf{eq}(\pi_1(\delta), n_A)$, $\mathbf{eq}(\pi_2(\delta)), B)$ and $\{\pi_1(\pi_2(\delta))\}_{\mathbf{pk}_B}^{n_2}$. We define $\delta', s'_\delta, a'_\delta, b'_\delta$ and $e'_\delta$ similarly.

We then rewrite $s$ and $s'$ into $s_\delta$ and $s'_\delta$ using $R$. Then we apply FA several times, first to deconstruct $s_\delta$ and $s'_\delta$, and then to deconstruct $a_\delta, b_\delta$ and $a'_\delta, b'_\delta$. Finally, we use Dup to remove duplicates, and we apply CCA2 simultaneously on key pairs ($pk_A, sk_A$) and ($pk_B, sk_B$) (we omit here the details of the syntactic side-conditions that have to be checked):

$$ \frac{\begin{array}{c} \phi_0, t_B[\mathbf{x}_B], n_A, \delta, e_\delta \sim \phi_0, t'_B[\mathbf{x}_B], n_A, \delta', e'_\delta \\ \phi_0, t_B[\mathbf{x}_B], a_\delta, b_\delta, e_\delta \sim \phi_0, t'_B[\mathbf{x}_B], a'_\delta, b'_\delta, e'_\delta \end{array}}{\phi_0, t_B[\mathbf{x}_B], s_\delta \sim \phi_0, t'_B[\mathbf{x}_B], s'_\delta} \quad \begin{array}{l} \text{CCA2} \\ (\text{FA, Dup})* \end{array} \\ \quad (\text{FA, Dup})* \quad R $$

## IV. MAIN RESULT AND DIFFICULTIES

We let $Ax$ be the conjunction of Struct-Ax and CCA2. We now state the main result of this paper.

**Theorem (Main Result).** *The following problem is decidable:*
*Input:* A ground formula $\vec{u} \sim \vec{v}$.
*Question:* Is $Ax \wedge \vec{u} \not\asymp \vec{v}$ unsatisfiable?

We give here an overview of the problems that have to be overcome in order to obtain the decidability result. Before starting, a few comments. We close all rules under permutations. The Sym rule commutes with all the other rules, and the CCA2 unitary axioms are closed under Sym. Therefore we can remove Perm and Sym from the set of rules. Observe that CS, FA, Dup and CCA2 are all decreasing rules, i.e. the premises are smaller than the conclusion. The only non-decreasing rules are $R$, which may rewrite a term into a larger one, and Restr, which we eliminate later. Therefore we now focus on $R$.
a) **Necessary Introductions:** As we saw in Example 2, it might be necessary to use $R$ in the “wrong direction”, typically to introduce new conditionals. A priori, this yields an unbounded search space. Therefore our goal is to characterize in which situations we need to use $R$ in the “wrong direction”, and with which instances. We identify two necessary reasons for introducing new conditionals.

First, to match the shape of the term on the other side, like $g()$ in Example 2. In this case, the introduced conditional is exactly the conditional that appeared on the other side of $\sim$. With more complex examples this may not be the case. Nonetheless, an introduced conditional is always bounded by the conditional it matches.

Second, we might introduce a guard in order to fit to the definition of safe decryptions in the CCA2 axioms, as in (3). Here also, the introduced guard will be of bounded size. Indeed, guards of $\text{dec}(s, sk)$ are of the form $\text{eq}(s, \alpha)$ where $\alpha$ is a subterm of $s$. Therefore, for a fixed $s$, there are a bounded number of them, and they are of bounded size.

**Example 3 (Cut Elimination).** These conditions are actually sufficient. We illustrate this on an example where the CS rule is applied on two conditionals that have just been introduced.

$$ \frac{a, s \sim b, t}{\text{if } a \text{ then } s \text{ else } s \sim \text{ if } b \text{ then } t \text{ else } t} \quad \begin{array}{c} \text{CS} \\ R \end{array} $$

Here $a$ and $b$ can be of arbitrary size. Intuitively, this is not a problem since any proof of $a, s \sim b, t$ includes a proof of $s \sim t$. Formally, we have the following weakening lemma.

**Lemma 1.** For every proof $P$ of a ground formula $\vec{u}, s \sim \vec{v}, t$, there exists a proof $P'$ of $\vec{u} \sim \vec{v}$ where $P'$ is no larger than $P$.

**Proof.** (sketch) The full proof is in the long version [25]. We prove by induction on $P$ that the $\text{Restr}$ rule is admissible using $\mathcal{A}X\{\text{Restr}\}$. For this to work, we need the CCA2 axioms to be closed under $\text{Restr}$. Note that this creates some problems, which are dealt with in [25]. ■

Using this lemma, we can deal with Example 3 by doing a proof cut elimination. More generally, by induction on the proof size, we can guarantee that no such proof cuts appear.

This is the strategy we are going to follow: look for proof cuts that introduce unbounded new terms, eliminate them, and show that after sufficiently many cut eliminations all the subterms appearing in the proof are bounded by the (R-normal form of the) conclusion.

But a proof may contain more complex behaviors than just the introduction of a conditional followed by a CS application. For example the conditional being matched could have been itself introduced earlier to match another conditional, which itself was introduced to match a third conditional etc.

**Example 4.** We illustrate this on an example. When it is more convenient, we write terms containing only `ifThen_else_` and other subterms (handled as constants) as binary trees; we also

index some subterms with a number, which helps keeping track of them across rule applications.

$$ \frac{a_1, b_2, b_3, u_4, w_5, u_6, v_7 \sim d_1, c_2, d_3, s_4, t_5, r_6, p_7}{\begin{array}{c} a_1 \\ b_2 \\ u_4 \\ w_5 \end{array} \sim \begin{array}{c} d_1 \\ c_2 \\ s_4 \\ t_5 \end{array} \quad \begin{array}{c} p_7 \\ v_7 \\ u_3 \\ u_6 \end{array}} \quad \text{FA}^{(3)} \\ \frac{\text{if } a \text{ then } u \text{ else } v \sim \text{ if } c \text{ then } s \text{ else } t}{} \quad R $$

where $p_7 \equiv \text{ if } c \text{ then } s \text{ else } t$. Here the conditionals $b, d$ and the terms $w, r$ are, a priori, arbitrary. Therefore we would like to bound them or remove them through a cut elimination. The cut elimination technique used in Example 3 does not apply here because we cannot extract a proof of $a \sim c$.

But we can extract a proof of $b_2, b_3 \sim c_2, d_3$. Using Proposition 1, this means that in every appropriate computational model, $[[b, b]] \approx [[c, d]]$. It means that no adversary can distinguish between getting twice the same value sampled from $[[b]]$ and getting a pair of values sampled from $[[c, d]]$. In particular, this means that $[[c]]_{\eta, \rho} = [[d]]_{\eta, \rho}$, except for a negligible number of random tapes $\rho$.

b) **A First Key Lemma:** A natural question is to ask whether this semantic equality $[[c]] = [[d]]$ implies a syntactic equality. While this is not the case in general, there are fragments of our logic in which this holds. We annotate the rules FA by the function symbol involved, and we let $\text{FA}_s = \{\text{FA}_f \mid f \in \mathcal{F}_s\}$.

**Definition 4.** Let $\Sigma$ be the set of axiom names, seen as an alphabet. For all $\mathcal{L} \subseteq \Sigma^*$, we let $\mathfrak{F}(\mathcal{L})$ be the fragment of our logic defined by: a formula $\phi$ is in the fragment iff there exists a proof $P$ such that $P \vdash \phi$ and, for every branch $\rho$ of $P$, the word $w$ obtained by collecting the axiom names along $\rho$ (starting from the root) is in $\mathcal{L}$.

**Lemma 2.** For all $b, b', b'', \text{ if } b, b \sim b', b''$ is in the fragment $\mathfrak{F}(\text{FA}_s^* \cdot \text{Dup}^* \cdot \text{CCA2})$ then $b' \equiv b''$.

**Proof.** The proof relies on the shape of the CCA2 axioms, and can be found in the long version [25]. ■

Using this lemma, we can deal with Example 4 if $a_1, b_2, b_3 \sim d_1, c_2, d_3$ lies in the fragment $\mathfrak{F}(\text{FA}_s^* \cdot \text{Dup}^* \cdot \text{CCA2})$. Using a first time the lemma on $b_2, b_3 \sim c_2, d_3$ we obtain $c \equiv d$, and using again the lemma on $a_1, b_2 \sim d_1, c_2$ (since $d \equiv c$) we deduce $a \equiv b$. Hence the cut elimination introduced before applies.

c) **Proof Sketch:** We now state the sketch of the proof:

* **Commutations:** first we show that we can assume that rules are applied in some given order. We prove this by showing some commutation results and adding new rules.

* **Proof Cut Eliminations:** through proof cut eliminations, we guarantee that every conditional appearing in the proof is $\alpha$-bounded. Intuitively a conditional is $\alpha$-bounded if it is a subterm of the conclusion or if it guards a decryption appearing in an $\alpha$-bounded term.
• **Decision Procedure:** we give a procedure that, given a goal formula $t \sim t'$, computes the set of $\alpha$-bounded terms for this formula. We show that this procedure computes a finite set, and deduce that the proof search is finite. This yields an effective algorithm to decide our problem.

## V. COMMUTATIONS AND CUT ELIMINATIONS

In this section we show, through rule commutations, that we can restrict ourselves to proofs using rules in some given order. Then, we show how this restricts the shapes of the terms.

### A. Rule Commutations

Everything in this subsection applies to any set $\mathcal{U}$ of unitary axioms closed under Restr. We specialize to CCA2 later.

We start by showing a set of rule commutations of the form $w \Rightarrow w'$, where $w$ and $w'$ are words over the set of rule names. An entry $w \Rightarrow w'$ means that a derivation in $w$ can be rewritten into a derivation in $w'$, with the same conclusion and premises. Here are the basic commutations we use:

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

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

**Lemma 3.** *All the above rule commutations are correct.*

*Proof.* We show only $\mathbf{FA} \cdot R \Rightarrow R \cdot \mathbf{FA}$ (the full proof is in the long version [25]):

$$ \frac{\frac{\vec{u}_1, \vec{v}_1 \sim \vec{u}'_1, \vec{v}'_1}{\vec{u}, \vec{v} \sim \vec{u}', \vec{v}'} R}{\vec{u}, f(\vec{v}) \sim \vec{u}', f(\vec{v}')} \text{FA} \Rightarrow \frac{\frac{\vec{u}_1, \vec{v}_1 \sim \vec{u}'_1, \vec{v}'_1}{\vec{u}_1, f(\vec{v}_1) \sim \vec{u}'_1, f(\vec{v}'_1)} \text{FA}}{\vec{u}, f(\vec{v}) \sim \vec{u}', f(\vec{v}')} R \text{■} $$

Using these rules, we obtain a first restriction.

**Lemma 4.** *The ordered strategy $\mathfrak{F}((\mathcal{CS} + R)^* \cdot \mathbf{FA}^* \cdot \text{Dup}^* \cdot \mathcal{U})$ is complete for $\mathfrak{F}((\mathcal{CS} + \mathbf{FA} + R + \text{Dup} + \mathcal{U})^*)$.*

*Proof.* First, we commute all the Dup to the right, which yields $\mathfrak{F}((\mathcal{CS} + R + \mathbf{FA})^* \cdot \text{Dup}^* \cdot \mathcal{U})$. Then, we commute all FA to the right, stopping at the first Dup. ■

a) **Splitting the FA Rule:** To go further, we split FA as follows: if the deconstructed symbol is `if_then_else_` then we denote the function application by $\text{FA}(b, b')$, where $b, b'$ are the involved conditionals; if the deconstructed symbol $f$ is in $\mathcal{F}_s$, then we denote the function application by $\text{FA}_f$. We give below the two new rules:

$$ \frac{\frac{\vec{w}, a, u, v \sim \vec{r}, b, s, t}{\vec{w}, \text{if } a \text{ then } u \text{ else } v} \text{FA}(b, b')}{\sim \vec{r}, \text{if } b \text{ then } s \text{ else } t} \text{FA}_f \frac{\vec{u}, \vec{v} \sim \vec{s}, \vec{t}}{\vec{u}, f(\vec{v}) \sim \vec{s}, f(\vec{t})} \text{FA}_f $$

The set of rule names is now infinite, since there exists one rule $\text{FA}(b, b')$ for every pair of ground terms $b, b'$.

b) **Further Commutations:** Intuitively, we want to use $R$ at the beginning of the proof only. This is helpful since, as we observed earlier, all the other rules are decreasing (i.e. premises are smaller than the conclusion). The problem is that we cannot fully commute $\mathcal{CS}$ and $R$. For example, in:

$$ \frac{\frac{a', u' \sim b', s'}{a, u \sim b, s} R}{\text{if } a \text{ then } u \text{ else } v \sim \text{ if } b \text{ then } s \text{ else } t} \frac{\frac{a'', v' \sim b'', t'}{a, v \sim b, t} R}{\text{CS}} $$

we can commute the rewritings on $u, v, s$ and $t$, but not on $a$ and $b$ because they appear twice in the premises, and $a'$ and $a''$ may be different (same for $b'$ and $b''$).

c) **New Rules:** We handle this problem by adding new rules to track relations between branches. We give only simplified versions here, the full rules are in the long version [25]. For every $a, c$ in $\mathcal{T}(\mathcal{F}_s, \mathcal{N})$ in $R$-normal form, we have the rules:

$$ \frac{\frac{\vec{u}, C[\underline{a|a}]_a \sim \vec{v}, C'[\underline{c|c}]_c}{\vec{u}, C[a] \sim \vec{v}, C'[c]} 2\text{Box}^s}{a_1, u \sim c_1, s} \frac{a_2, v \sim c_2, t}{\text{if } [a_1 \underline{a_2}]_a \text{ then } u \text{ else } v \sim \text{ if } [c_1 \underline{c_2}]_c \text{ then } s \text{ else } t} \text{CS}_\square^s $$

where $\square\square a$ is a new symbol of sort $S_b^2 \to S_b$, and of fixed semantics: it ignores its arguments and has the semantics $[[a]]$. Intuitively, $[a_1 \underline{a_2}]_a$ stands for the conditional $a$, and $a_1, a_2$ are, respectively, the left and right versions of $a$.

Remark that for the $\mathcal{CS}_\square$ rule to be sound we need $[[a_1]]$, $[[a_2]]$ and $[[a]]$ to be equal, up to a negligible number of samplings (same for $c_1, c_2$ and $c$). This is not enforced by the rules, so it has to be an invariant of our strategy. We denote $\mathcal{B}$ the set of new function symbols. We need the functions in $\mathcal{B}$ to block the if-homomorphism to ensure that for all $[a|c]_b \in \text{st}(t)$, $[[a]] = [[c]] = [[b]]$. Therefore the TRS $R_2$ is not extended to $\mathcal{B}$. For example we have:

$$ \text{if } a \text{ then } c \text{ else } d \text{ [e]}_b \Leftrightarrow_R^* \text{ if } a \text{ then } c \text{ [e]}_b \text{ else } d \text{ [e]}_b $$

The $R$ rule is replaced by $R_\square$ which has an extra side-condition. $R_\square$ can rewrite $u[s]$ into $u[t]$ as long as:

$$ \{ [a|c]_b \in \text{st}(t) \} \subseteq \{ [a|c]_b \in \text{st}(u[s]) \} $$

This ensures that no new arbitrary $[a|c]_b$ is introduced. New boxed conditionals are only introduced through the 2Box rule. Similarly, the $\mathbf{FA}$ axiom is not extended to $\mathcal{B}$.

**Definition 5.** A term $t$ is well-formed if for every $[a|c]_b \in \text{st}(t)$, $a =_R c =_R b$. We lift this to formulas as expected.

**Proposition 4.** *The following rules preserve well-formedness:*

$$ R_\square, 2\text{Box}, \mathcal{CS}_\square, \text{FA}_s, \{\text{FA}(b, b')\}, \text{Dup} $$

Besides, $R_\square$, $\mathcal{CS}_\square$ and $2\text{Box}$ are sound on well-formed formulas.

*Proof.* The only rule not obviously preserving well-formedness is $R_\square$, but its side-conditions guarantee the well-formedness invariant. The only rule that is not always sound is $\mathcal{CS}_\square$, and it is trivially sound on well-formed formulas. ■
d) Ordered Strategy: We have new rule commutations.

$$ \begin{array}{lcl} \mathsf{FA}_s \cdot \mathsf{FA}(b, b') & \Rightarrow & \mathsf{R} \cdot \mathsf{FA}(b, b') \cdot \mathsf{FA}_s^* \cdot \mathsf{Dup} \\ \mathsf{CS}_\square \cdot \mathsf{R}_\square & \Rightarrow & \mathsf{R}_\square \cdot \mathsf{CS}_\square \\ \mathsf{CS}_\square \cdot 2\mathsf{Box} & \Rightarrow & \mathsf{R}_\square \cdot 2\mathsf{Box} \cdot \mathsf{CS}_\square \end{array} $$

$$ \begin{array}{lcl} \mathsf{CS}_\square \cdot \mathsf{R}_\square & \Rightarrow & \mathsf{R}_\square \cdot \mathsf{CS}_\square \\ \mathsf{CS}_\square \cdot 2\mathsf{Box} & \Rightarrow & \mathsf{R}_\square \cdot 2\mathsf{Box} \cdot \mathsf{CS}_\square \end{array} $$

**Lemma 5.** All the rule commutations above are correct.

*Proof.* The proof can be found in the long version [25].

This allows to have $R_\square$ rules only at the beginning of the proof.

**Lemma 6.** The ordered strategy:

$$ \mathfrak{F}((2\mathsf{Box} + R_\square)^* \cdot \mathsf{CS}_\square^* \cdot \{\mathsf{FA}(b, b')\}^* \cdot \mathsf{FA}_s^* \cdot \mathsf{Dup}^* \cdot \mathsf{U}) $$

is complete for $\mathfrak{F}((\mathsf{CS} + \mathsf{FA} + \mathsf{R} + \mathsf{Dup} + \mathsf{U})^*)$.

*Proof.* We start from the result of Lemma 4, split the FA rules and commute rules until we get:

$$ \mathfrak{F}((\mathsf{CS} + \mathsf{R})^* \cdot \{\mathsf{FA}(b, b')\}^* \cdot \mathsf{FA}_s^* \cdot \mathsf{Dup}^* \cdot \mathsf{U}) $$

We then replace all applications of $\mathsf{CS}$ by $2\mathsf{Box} \cdot \mathsf{CS}_\square$. All $\underline{a|a}_a$ introduced are immediately “opened” by a $\mathsf{CS}_\square$ application, hence we know that the side-conditions of $R_\square$ hold every time we apply $\mathsf{R}$. Therefore we can replace all applications of $\mathsf{R}$ by $R_\square$, which yields:

$$ \mathfrak{F}((\mathsf{CS}_\square + 2\mathsf{Box} + R_\square)^* \cdot \{\mathsf{FA}(b, b')\}^* \cdot \mathsf{FA}_s^* \cdot \mathsf{Dup}^* \cdot \mathsf{U}) $$

Finally we commute the $\mathsf{CS}_\square$ applications to the right.

B. The Freeze Strategy

We now show that we can restrict the terms on which the rules in $\{\mathsf{FA}(b, b')\}$ can be applied: when we apply a rule in $\{\mathsf{FA}(b, b')\}$, we “freeze” the conditionals $b$ and $b'$ to forbid any further applications of $\{\mathsf{FA}(b, b')\}$ to them.

*Example 5.* Let $a_i \equiv$ if $b_i$ then $c_i$ else $d_i$ ($i \in \{1, 2\}$), we want to forbid the following partial derivation to appear:

$$ \frac{\frac{b_1, c_1, d_1, u_1, v_1 \sim b_2, c_2, d_2, u_2, v_2}{a_1, u_1, v_1 \sim a_2, u_2, v_2}}{\text{if } a_1 \text{ then } u_1 \text{ else } v_1 \sim \text{if } a_2 \text{ then } u_2 \text{ else } v_2} \mathsf{FA}(b_1, b_2) \mathsf{FA}(a_1, a_2) $$

a) Freeze Strategy: We let $\bar{s}$ be a new function symbol of arity one, and for every ground term $s$ we let $\tilde{s}$ be the term:

$$ \tilde{s} \equiv \left\{ \begin{array}{ll} \text{if } \bar{b} \text{ then } u \text{ else } v & \text{if } s \equiv \text{if } b \text{ then } u \text{ else } v \\ s & \text{if } s \in \mathcal{T}(\mathcal{F}_s, \mathcal{N}) \end{array} \right. $$

Moreover we replace every $\mathsf{FA}(b_1, b_2)$ rule by the rule:

$$ \frac{\frac{\tilde{w}_1, \tilde{b}_1, u_1, v_1 \sim \tilde{w}_2, \tilde{b}_2, u_2, v_2}{\tilde{w}_1, \text{if } b_1 \text{ then } u_1 \text{ else } v_1 \sim \tilde{w}_2, \text{if } b_2 \text{ then } u_2 \text{ else } v_2}}{\mathsf{BFA}(b_1, b_2)} $$

We let $\{\overline{\mathsf{BFA}}(b_1, b_2)\}$ be the restriction of $\{\mathsf{BFA}(b_1, b_2)\}$ to the rules where $b_1$ and $b_2$ are not frozen conditionals. Finally, we add a new rule, UnF, which unfreezes all conditionals: every $\bar{b}$ is replaced by $b$.

**Lemma 7.** The following strategy:

$$ \mathfrak{F}((2\mathsf{Box} + R_\square)^* \cdot \mathsf{CS}_\square^* \cdot \{\overline{\mathsf{BFA}}(b, b')\}^* \cdot \mathsf{UnF} \cdot \mathsf{FA}_s^* \cdot \mathsf{Dup}^* \cdot \mathsf{U}) $$

is complete for $\mathfrak{F}((\mathsf{CS} + \mathsf{FA} + \mathsf{R} + \mathsf{Dup} + \mathsf{U})^*)$.

*Proof.* Basically, the proof consists in eliminating all proof cuts of the shape given in Example 5. The cut elimination is simple, though voluminous, and is given in the long version [25].

VI. PROOF FORM AND KEY PROPERTIES

The goal of this section is to show that we can assume w.l.o.g. that the terms appearing in the proof (following the ordered freeze strategy) after the $(2\mathsf{Box} + R_\square)^*$ part have a particular form, that we call proof form. We also show properties of this restricted shape that allow more cut eliminations.

A. Shape of the Terms

Most of the completeness results shown before are for any set of unitary axioms closed under Restr. We now specialize these results to CCA2, to get some further restrictions.

When applying the unitary axioms CCA2, we would like to require that terms are in $\mathsf{R}$-normal form, e.g. to avoid the application of CCA2 to terms with an unbounded component, such as $\pi_1(\langle u, v \rangle)$. Unfortunately, the side-conditions of CCA2 are not stable under $\mathsf{R}$. E.g., consider the CCA2 instance:

$$ \frac{\{\text{if } \mathsf{eq}(g(n_u), n_u) \text{ then } A \text{ else } B\}_{\mathsf{pk}(n)}^{n_r} \sim \{C\}_{\mathsf{pk}(n)}^{n_r}}{\mathsf{CCA2}} $$

The $\mathsf{R}$-normal form of the left term is:

$$ \text{if } \mathsf{eq}(g(n_u), n_u) \text{ then } \{A\}_{\mathsf{pk}(n)}^{n_r} \text{ else } \{B\}_{\mathsf{pk}(n)}^{n_r} $$

which cannot be used in a valid CCA2 instance, since the conditional $\mathsf{eq}(g(n_u), n_u)$ should be somehow “hidden” by the encryption. To avoid this difficulty, we use a different normal form for terms: we try to be as close as possible to the $\mathsf{R}$-normal form, while keeping conditional branching below their encryption. First, we illustrate this on an example. The term:

$$ \{\text{if } (\text{if } b \text{ then } a \text{ else } c) \text{ then } \{\text{if } d \text{ then } u \text{ else } v\}_{\mathsf{pk}}^{n_1} \text{ else } w\}_{\mathsf{pk}}^{n_2} $$

is normalized as follows:

$$ \left\{ \begin{array}{l} \text{if } b \text{ then if } a \text{ then } \{\text{if } d \text{ then } u \text{ else } v\}_{\mathsf{pk}}^{n_1} \text{ else } w \\ \text{else if } c \text{ then } \{\text{if } d \text{ then } u \text{ else } v\}_{\mathsf{pk}}^{n_1} \text{ else } w \end{array} \right\}_{\mathsf{pk}}^{n_2} $$

a) Basic Terms: We omit the rewriting strategy here, and describe instead the properties of the normalized terms. We let $\mathcal{A}_>$ be the ordered strategy from Lemma 7, and $\mathcal{A}_{\mathsf{CS}_\square}$ be its restriction to proofs with an empty $(2\mathsf{Box} + R_\square)^*$ part. The rule $\mathsf{CS}_\square$ is the only branching rule, therefore, after applying all the $\mathsf{CS}_\square$ rules, we can associate to each branch $l$ of the proof an instance $S_l = (\mathcal{K}_l, \mathcal{R}_l, \mathcal{E}_l, \mathcal{D}_l)$ of the CCA2 axiom, where $\mathcal{K}_l, \mathcal{R}_l, \mathcal{E}_l$ and $\mathcal{D}_l$ are the sets of, respectively, secret keys, encryption randomness, encryptions and decryptions. We use $S_l$ to define a normal form for the terms appearing in branch $l$. This is done through four mutually inductive definitions: $S_l$-encryption oracle calls are well-formed encryptions; $S_l$-decryption oracle calls are well-formed decryptions; $S_l$-normalized basic terms are terms built using function symbols in $\mathcal{F}_s$ and well-formed encryptions and decryptions; and $S_l$-normalized simple terms are combinations
<figure><img src="image_7.png" /><figcaption>Fig. 4. The shape of the term is determined by the proof.</figcaption></figure>

of normalized basic terms using `ifThenElse`. We give only the definition of $S_l$-normalized basic terms (the full definitions are in the long version [25]).

**Definition 6.** A $S_l$-normalized basic term is a term $t$ of the form $U[\vec{w}, (\alpha_j)_j, (dec_k)_k]$ where:

* $U$ and $\vec{w}$ are if-free and $R_l, K_l$ do not appear in $\vec{w}$.

* $U[\vec{w}, (\{[]_j\}_{pk_j}^{n_j})_j, (dec([k], sk_k))_k]$ is in $R$-normal form.

* $(\alpha_j)_j$ are $S_l$-encryption oracle calls under $(pk_j, sk_j)_j$.

* $(dec_k)_k$ are $S_l$-decryption oracle calls under $(pk_k, sk_k)_k$.

If $t$ is of sort `bool`, we say that it is a $S_l$-normalized basic conditional.

**b) Normalized Proof Form:** Every application of $CS_\square$:

$$ \frac{a_1, u \sim b_1, s \qquad a_2, v \sim b_2, t}{\text{if } [a_1 \mid a_2]_a \text{ then } u \text{ else } v \sim \text{if } [b_1 \mid b_2]_b \text{ then } s \text{ else } t} \text{CS}_\square $$

is such that if we extract the sub-proof of $a_i \sim b_i$ (for $i \in \{1, 2\}$), we get a proof in $A_{CS_\square}$. Therefore, we can check that terms after $(2\Box x + R_\square)^*$ are of the form informally described in Fig. 4. We define a normal form for such proofs, called *normalized proof form*, and we define $\vdash^{\text{npf}}$ by $P \vdash^{\text{npf}} t \sim t'$ if and only if $P \vdash t \sim t'$, the proof $P$ is in $A_>$ and is in *normalized proof form*. We do not give the full definition, but one of the key ingredients is to require that for every term $s$ appearing in a branch $l$ of the proof $P$, if $s$ is the conclusion of a sub-proof in the fragment $\mathfrak{F}(\mathrm{FA}_s^* \cdot \mathrm{Dup}^* \cdot \mathrm{U})$ then $s$ is a $S_l$-normalized basic term.

**Lemma 8.** Every formula in $\mathfrak{F}((CS + FA + R + Dup + CCA2)^*)$ is provable using the strategy $\vdash^{\text{npf}}$.

**Proof. (sketch)** The full proof is in the long version [25]. First, we rewrite terms by pulling conditionals upward without crossing an encryption function symbol, and without modifying decryption guards. Then, we remove all redexes from $R_1$ (e.g. $\pi_1(\langle u, v \rangle) \rightarrow u$) using a cut elimination procedure. E.g., the following cut can be eliminated using Lemma 1:

$$ \frac{u, v \sim u', v' \qquad \frac{\pi_1(\langle u, v \rangle) \sim \pi_1(\langle u', v' \rangle)}{u \sim u'}}{FA(\langle, \rangle)} \qquad R $$

## B. Key Properties

A term in $R$-normal form is in the following grammar:

$$ t ::= u \in \mathcal{T}(\mathcal{F}_s, \mathcal{N}) \mid \text{if } b \text{ then } t \text{ else } t \text{ (with } b \in \mathcal{T}(\mathcal{F}_s, \mathcal{N})\text{)} $$

Given a term $t$ in $R$-normal form, we let cond-st($t$) be its set of conditionals, and leave-st($t$) its set of leaves.

**a) Characterization of Basic Terms:** We give a key characterization proposition for basic terms: if two $S_l$-normalized basic terms $\beta$ and $\beta'$ are such that, when $R$-normalizing them, they share a leaf term, then they are identical.

**Proposition 5.** For all $S_l$-normalized basic terms $\beta, \beta'$, if we have leave-st($\beta \downarrow_R$) $\cap$ leave-st($\beta' \downarrow_R$) $\neq \emptyset$ then $\beta \equiv \beta'$.

**Proof. (sketch)** The full proof is in the long version [25]. We give the intuition: since they are $S_l$-normalized basic terms, we know that $\beta \equiv U[\vec{w}, (\alpha_j)_j, (dec_k)_k]$, $\beta' \equiv U'[\vec{w}', (\alpha'_j)_j, (dec'_k)_k]$ and:

$$ \begin{align*} U[\vec{w}, (\{[]_j\}_{pk_j}^{n_j})_j, (dec([k], sk_k))_k] \\ U'[\vec{w}', (\{[]'_j\}_{pk'_j}^{n'_j})_j, (dec([k'], sk'_k))_k] \end{align*} $$

are in $R$-normal form. Using the fact that $U, U', \vec{w}, \vec{w}'$ are if-free, and the hypothesis that $\beta$ and $\beta'$ share a leaf term, we first show that we can assume $U \equiv U'$ and $\vec{w} \equiv \vec{w}'$ by induction on the number of positions where $U$ and $U'$ differ. Take $p$ where they differ, w.l.o.g. assume $\beta'_p$ to be a hole of $U'$ (otherwise swap $\beta$ and $\beta'$). We have three cases: i) if $\beta'_p$ is in $\vec{w}$, we simply change $U$ to include everything up to $p$; ii) if $\beta'_p$ is in some encryption $\alpha_j \equiv \{m\}_{pk_j}^n$, then we know that $n$ appears in $\vec{w}$, which is not possible since, as $\beta$ is a $S_l$-normalized basic term, $n \in \mathcal{R}_l$ does not appear in $\vec{w}$; iii) if $\beta'_p$ is in some decryption $dec_k \equiv dec(u_k, sk_k)$ then, similarly to the previous case, we have $sk_k$ appearing in $\vec{w}$, which contradicts the fact that $sk_k \in K_l$ do not appear in $\vec{w}$.

Knowing that $U \equiv U'$ and $\vec{w} \equiv \vec{w}'$, it only remains to show that the encryptions $(\alpha_j)_j$ and $(\alpha'_j)_j$, and the decryptions $(dec_k)_k$ and $(dec'_k)_k$ are identical. The former follows from the fact that, for a given encryption randomness $n \in \mathcal{R}_l$, there exists a unique $m$ such $\{m\}_n \in \mathcal{E}_l$; and the latter follows from the fact that there is a unique way to guard a decryption in $\mathcal{D}_l$ (this is not obvious, and relies on CCA2 side-conditions). ■

**b) Proofs of $b \sim \text{false or true}$:** Using the previous proposition, we can show that for all $b$, if $b$ is if-free then there is no derivation of $b \sim \text{true}$ or $b \sim \text{false}$ in $A_>$. Such derivations would be problematic since true and false are conditionals of constant size, but $b$ could be of any size (and we are trying to bound all conditionals appearing in a proof). Also, the else branch of a true conditional can contain anything and is, a priori, not bounded by the proof conclusion.

**Proposition 6.** Let $b$ an if-free conditional in $R$-normal form, with $b \not\equiv \text{false}$ (resp. $b \not\equiv \text{true}$). Then there exists no derivation of $b \sim \text{false}$ (resp. $b \sim \text{true}$) in $A_>$.

**Proof.** This is shown by induction on the size of the derivation. The full proof is in the long version [25], and relies on Proposition 5. ■
VII. BOUNDING THE PROOF AND DECISION PROCEDURE

We give here two similar proof cut eliminations, one used on $\overline{\text{BFA}}$ conditionals and the other on $\text{CS}_\square$ conditionals.

a) **$\overline{\text{BFA}}$ Rule:** We already used this cut elimination to deal with Example 4 for conditionals involved in $\overline{\text{BFA}}$ applications. The cuts we want to eliminate are of the form:

$$ \frac{a_1, a_2, u_3, v_4, w_5 \sim b_1, c_2, r_3, s_4, t_5}{\begin{array}{c} a_1 \\ a_2 \\ u_3 \\ \underbrace{\phantom{a_1}}_{\sigma} \end{array}} \sim \frac{b_1}{\begin{array}{c} c_2 \\ r_3 \\ \underbrace{\phantom{c_2}}_{\tau} \end{array}} \sim \frac{t_5}{\begin{array}{c} s_4 \\ \underbrace{\phantom{t_5}}_{\tau} \end{array}} \qquad \overline{\text{BFA}}^{(2)} \qquad (4) $$

Using Lemma 1, we extract a proof of $a_1, a_2 \sim b_1, c_2$, which, thanks to the ordered strategy, is in $\mathfrak{F}(\text{FA}_s^* \cdot \text{Dup}^* \cdot \text{CCA2})$. From Lemma 2 we get that $b \equiv c$. We then replace (4) by:

$$ \frac{a_1, u_3, w_5 \sim b_1, r_3, t_5}{\begin{array}{c} a_1 \\ u_3 \\ \underbrace{\phantom{a_1}}_{\sigma} \end{array}} \sim \frac{b_1}{\begin{array}{c} r_3 \\ \underbrace{\phantom{r_3}}_{\tau} \end{array}} \sim \frac{t_5}{R} \qquad \overline{\text{BFA}} \qquad (5) $$

We retrieve a proof in $\mathcal{A}_>$ by pulling $R$ to the beginning of the proof.

b) **$\text{CS}_\square$ Rule:** The $\text{CS}_\square$ case is more complicated. E.g., take two boxed $\text{CS}_\square$ conditionals for the same if-free conditional $a$, and two arbitrary $\text{CS}_\square$ conditionals on the right side:

$$ a_i^\square \equiv \boxed{a_1^l \quad a_1^r}_a \quad (i \in \{1, 2\}) \qquad b_1^\square \equiv \boxed{b_1^l \quad b_1^r}_b \qquad c_2^\square \equiv \boxed{c_2^l \quad c_2^r}_c $$

Consider the following cut:

$$ \frac{\begin{array}{c} \vdots (A) \\ a_1^l, a_2^l, u_3 \sim b_1^l, c_2^l, r_3 \\ \begin{array}{c} a_1^\square \\ a_2^\square \\ u_3 \end{array} \\ \underbrace{\phantom{a_1^\square}}_{\sigma} \end{array}}{\begin{array}{c} \vdots (B) \\ a_1^l, a_2^l, v_4 \sim b_1^l, c_2^l, s_4 \\ \begin{array}{c} b_1^\square \\ c_2^\square \\ r_3 \end{array} \\ \underbrace{\phantom{b_1^\square}}_{\tau} \end{array}} \sim \frac{\begin{array}{c} \vdots (C) \\ a_1^r, w_5 \sim b_1^r, t_5 \\ \begin{array}{c} t_5 \\ \underbrace{\phantom{t_5}}_{\tau} \end{array} \end{array}}{\begin{array}{c} \text{CS}_\square^{(2)} \\ \begin{array}{c} c_2^l \\ \underbrace{\phantom{c_2^l}}_{\tau} \end{array} \end{array}} \qquad (6) $$

As we did for $\overline{\text{BFA}}$, we can extract from $(A)$, using Lemma 1, a proof of $a_1^l, a_2^l \sim b_1^l, c_2^l$. But using the ordered strategy, we get that this proof is in $\mathcal{A}_{\text{CS}_\square}$, which we recall is the fragment:

$$ \text{CS}_\square^* \cdot \{\overline{\text{BFA}}(b, b')\}^* \cdot \text{UnF} \cdot \text{FA}_s^* \cdot \text{Dup}^* \cdot \text{CCA2} $$

Therefore we cannot apply Lemma 2. To deal with this cut, we generalize Lemma 2 to the case where the proof is in $\mathcal{A}_{\text{CS}_\square}$. For this, we need the extra assumptions that $a_1^l, a_2^l, b_1^l, c_2^l$ are if-free, which is a side-condition of $\text{CS}_\square$.

**Lemma 9.** For all $a, a', b, c$ such that their R-normal form is if-free and $a =_R a'$, if $P \vdash^{\text{npf}} a, a' \sim b, c$ then $b =_R c$.

*Proof.* (sketch) The full proof is given in the long version [25]. It uses Proposition 6 to obtain a proof $P'$ of $a, a' \sim b, c$ without any **false** and **true**, and also relies on Proposition 5 and Lemma 2. ■

We now deal with the cut above. Using Lemma 9, we know that $b =_R c$. Since $b, c$ are in R-normal form, $b \equiv c$ and therefore $b_1^\square =_R b =_R c_2^\square$ (using well-formedness). Similarly $a_1^\square =_R a =_R a_2^\square$. This yields the (cut-free) proof:

$$ \frac{\begin{array}{c} \vdots (A') \\ a_1^l, u_3 \sim b_1^l, r_3 \\ \begin{array}{c} a_1^\square \\ u_3 \end{array} \\ \underbrace{\phantom{a_1^\square}}_{\sigma} \end{array}}{\begin{array}{c} \vdots (C) \\ a_1^r, w_5 \sim b_1^r, t_5 \\ \begin{array}{c} b_1^\square \\ r_3 \end{array} \\ \underbrace{\phantom{b_1^\square}}_{\tau} \end{array}} \sim \frac{\begin{array}{c} \text{CS}_\square \\ R \end{array}}{\sigma \sim \tau} \qquad (7) $$

where $(A')$ is extracted from $(A)$ by Lemma 1. Finally, to get a proof in $\mathcal{A}_>$, we commute the $R_\square$ rewriting to the beginning.

A. Decision Procedure

Now, we explain how we obtain a decision procedure for our logic. Because the proofs and definitions are long and technical, we omit most of the details and focus instead on giving a high level sketch of the proof and decision procedure.

a) **Spurious Conditionals:** A conditional $b$ without if-then-else and in R-normal form is said to be spurious in $t$ if, when R-normalizing $t$, the conditional $b$ disappears. Formally, $b$ is spurious in $t$ if $b \notin \text{cond-st}(t \downarrow_R)$. E.g., the conditional $\text{eq}(n_0, n_1)$ is spurious in:

if $\text{eq}(n_0, n_1)$ then $g(n)$ else $g(n)$

We say that a basic conditional $\beta$, which may not be if-free, is spurious in $t$ if all its leaf terms are spurious in $t$ (i.e. leave-st($\beta \downarrow_R$) $\cap$ cond-st($t \downarrow_R$) $= \emptyset$). As we saw in Example 2, we may need to introduce spurious basic conditionals to carry out a proof. Still, we need to bound such terms. To do this, we characterize the basic conditionals that cannot be removed: basically, a basic conditional is $\alpha$-bounded in a proof of $t \sim t'$ if it is not spurious in $t$ or $t'$, or if it is a guard for a decryption appearing in a $\alpha$-bounded conditional of $t \sim t'$ (indeed, we cannot remove a decryption's guards, as this would not yield a valid CCA2 instance).

We let $\vdash_{\alpha}^{\text{npf}}$ be the restriction of $\vdash^{\text{npf}}$ to proofs such that all basic conditionals appearing in the derivation are $\alpha$-bounded. Using the cut eliminations we introduced earlier, plus some additional cut eliminations, we can show the following completeness result (the full proof is in the long version [25]).

**Lemma 10.** $\vdash_{\alpha}^{\text{npf}}$ is complete with respect to $\vdash^{\text{npf}}$.

b) **Bounding $\alpha$-bounded Basic Conditionals:** Finally, it remains to bound the size of $\alpha$-bounded basic conditionals. Since basic conditionals can be nested (e.g. a basic conditional can contain decryption guards, which are themselves basic conditionals etc), we need to bound the length of sequences of nested basic conditionals.

Given a sequence of nested basic conditionals $\beta_1 <_{\text{st}} \cdots <_{\text{st}} \beta_n$, (where $u <_{\text{st}} v$ iff $u \neq v$ and $u \in \text{st}(v)$), we show that we can associate to each $\beta_i$ a “frame term” $\lambda_i \in \mathcal{B}(t, t')$ (where $\mathcal{B}(t, t')$ is a set of terms of bounded size w.r.t. $|t| + |t'|$). Basically, $\lambda_i$ is obtained from $\beta_i$ by
“flattening” it: we remove all decryption guards, and replace the content of every encryption {$m$}npk by a term {$\tilde{m}$}npk, where $\tilde{m}$ is if-free and in $\mathcal{B}(t, t')$. Moreover, we show that, for every $S_l$-normalized basic terms $\beta, \gamma$ and their associated frame terms $\lambda, \mu$, if $\lambda \equiv \mu$ then $\beta \equiv \gamma$ (this result is similar to Proposition 5).

Since the $\beta_i$s are all pair-wise distinct (as $<_{st}$ is strict), and since for every $i$, the frame term $\lambda_i$ uniquely characterizes $\beta_i$, we know that the $\lambda_i$s are pair-wise distinct. Using a pigeon-hole argument, this shows that $n \le |\mathcal{B}(t, t')|$. Then, by induction on the number of nested basic conditionals, we show a triple exponential upper-bound in $|t|+|t'|$ on the size of the basic conditionals appearing in a cut-free proof of $t \sim t'$.

c) *Decision Procedure:* To conclude, we show that there exists a non-deterministic procedure that, given two terms $t$ and $t'$, non-deterministically guesses a set of $\alpha$-bounded basic terms that can appear in a proof $P$ of $P |_{\alpha}^{\text{npf}} t \sim t'$ (in triple exponential time in $|t| + |t'|$). Then the procedure guesses the rule applications, and checks that the candidate derivation is a valid proof (in polynomial time in the candidate derivation size). This yields a 3-\textit{NEXPTIME} decision procedure that shows the decidability of our problem.

**Theorem (Main Result).** *The following problem is decidable:*
*Input:* A ground formula $\vec{u} \sim \vec{v}$.
*Question:* Is $Ax \wedge \vec{u} \not\sim \vec{v}$ unsatisfiable?

VIII. RELATED WORKS

In [29], the authors design a set of inference rules to prove CPA and CCA security of asymmetric encryption schemes in the Random Oracle Model. The paper also presents an attack finding algorithm. The authors of [29] do not provide decision algorithm for the designed inference rules. However, they designed proof search heuristics and implemented an automated tool, called ZooCrypt, to synthesize new CCA encryption schemes. For small schemes, this procedure can show CCA security or find an attack in more than 80% of the cases. In 20% of the cases, security remains undecided. Additionally, ZooCrypt automatically generates concrete security bounds.

As seen in the introduction, the problem of showing CPA security can be cast into the BC logic. Take a candidate encryption scheme $x \mapsto t[x]$, where $t[$ is a context built using, e.g., pairs, a one-way permutation $f$ using public key pk(n), hash functions and xor. Then this scheme is CPA if the following formula is valid in every computational model satisfying some implementation assumptions (mostly, $f$ is OW-CPA and the hash functions are PRF):

$$t[\pi_1(f(\mathbf{pk}(n)))] \sim t[\pi_2(f(\mathbf{pk}(n)))]$$

This formula has a particular shape, which stems from the limitations on the adversary's interactions: the adversary can only interact with the (candidate) encryption scheme through the CPA or CCA game. There is no complex and arbitrary interactions with the adversary, as it is the case with a security protocol. We don't have such restrictions.

In [30], the authors study proof automation in the UC framework [31]. They design a complete procedure for deciding the

existence of a simulator, for ideal and real functionalities using if-then-else, equality, random samplings and xor. Therefore their algorithm cannot be used to analyse functionalities relying on more complex functions (e.g., public key encryption), or stateful functionalities. This restricts the protocols that can be checked. Still, their method is semantically complete (while we are complete w.r.t. a fixed set of inference rules): if there exists a simulator, they will find it.

In [32], the authors show the decidability of the problem of the equality of two distributions, for a specific equational theory (concatenation, projection and xor). Then, for arbitrary equational theories, they design a proof system for proving the equality of two distributions. This second contribution has similarities with our work, but differ in two ways.

First, the proof system of [32] shares some rules with ours, e.g. the $R$, Dup and FA rules. But it does not allow for reasoning on terms using `ifThen_else_`. E.g., they do not have a counterpart to the `CS` rule. This is a major difference, as most of the difficulties encountered in the design of our decision procedure result from the `ifThen_else_` conditionals. Moreover, there are no rules corresponding to cryptographic assumptions, as our CCA2 rules. Because of this and the lack of support for reasoning on branching terms, the analysis of security protocols is out of the scope of [32].

Second, the authors do not provide a decision procedure for their inference rules, but instead rely on heuristics.

IX. CONCLUSION

We designed a decision procedure for the Bana-Comon indistinguishability logic. This allows to automatically verify that a security protocol satisfies some security property. Our result can be reinterpreted, in the cryptographic game transformation setting, as a cut elimination procedure that guarantees that all intermediate games introduced in a proof are of bounded size w.r.t. the protocol studied.

A lot of work remains to be done. First, our decision procedure is in 3-\textit{NEXPTIME}, which is a high complexity. But, as we do not have any lower-bound, there may exist a more efficient decision procedure. Finding such a lower-bound is another interesting direction of research. Then, our completeness result was proven for CCA2 only. We believe it can be extended to more primitives and cryptographic assumptions. For example, signatures and EUF-CMA are very similar to asymmetric encryption and IND-CCA2, and should be easy to handle (even combined with the CCA2 axioms).

ACKNOWLEDGMENT

We thank Hubert Comon for his help and useful comments.

This research has been partially funded by the French National Research Agency (ANR) under the project TECAP (ANR-17-CE39-0004-01).

REFERENCES

[1] G. Bana and H. Comon-Lundh, “A computationally complete symbolic attacker for equivalence properties,” in 2014 ACM Conference on Computer and Communications Security, CCS ’14. ACM, 2014, pp. 609–620.
[2] G. Bana and H. Comon-Lundh, "Towards unconditional soundness: Computationally Complete Symbolic Attacker," in *Principles of Security and Trust*, 2012, ser. LNCS, vol. 7215. Springer, 2012, pp. 189–208.

[3] D. Adrian, K. Bhargavan, Z. Durumeric, P. Gaudry, M. Green, J. A. Halderman, N. Heninger, D. Springall, E. Thomé, L. Valenta, B. VanderSloot, E. Wustrow, S. Z. Béguelin, and P. Zimmermann, "Imperfect forward secrecy: How Diffie-Hellman fails in practice," in *ACM Conference on Computer and Communications Security*. ACM, 2015, pp. 5–17.

[4] K. Bhargavan, A. Delignat-Lavaud, C. Fournet, A. Pironti, and P. Strub, "Triple handshakes and cookie cutters: Breaking and fixing authentication over TLS," in *IEEE Symposium on Security and Privacy*. IEEE Computer Society, 2014, pp. 98–113.

[5] B. Blanchet, PROVERIF: Cryptographic protocols verifier in the formal model, available at http://prosecco.gforge.inria.fr/personal/bblanchet/proverif/.

[6] S. Meier, B. Schmidt, C. Cremers, and D. Basin, "The TAMARIN prover for the symbolic analysis of security protocols," in *25th International Conference on Computer Aided Verification, CAV'13*. Springer-Verlag, 2013, pp. 696–701.

[7] V. Cheval, S. Kremer, and I. Rakotonirina, "DEEPSEC: deciding equivalence properties in security protocols theory and practice," in *2018 IEEE Symposium on Security and Privacy, SP 2018*. IEEE, 2018, pp. 529–546.

[8] G. Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin, "Computer-aided security proofs for the working cryptographer," in *Advances in Cryptology - CRYPTO, 2011*, ser. LNCS, vol. 6841. Springer, 2011, pp. 71–90.

[9] B. Blanchet, "A computationally sound mechanized prover for security protocols," *IEEE Trans. Dependable Sec. Comput.*, vol. 5, no. 4, pp. 193–207, 2008.

[10] H. Comon-Lundh, V. Cortier, and E. Zalinescu, "Deciding security properties for cryptographic protocols. application to key cycles," *ACM Trans. Comput. Log.*, vol. 11, no. 2, pp. 9:1–9:42, 2010.

[11] E. D'Osualdo, L. Ong, and A. Tiu, "Deciding secrecy of security protocols for an unbounded number of sessions: The case of depth-bounded processes," in *CSF*. IEEE Computer Society, 2017, pp. 464–480.

[12] A. Finkel and P. Schnoebelen, "Well-structured transition systems everywhere!" *Theor. Comput. Sci.*, vol. 256, no. 1-2, pp. 63–92, 2001.

[13] R. Chrétien, V. Cortier, and S. Delaune, "Decidability of trace equivalence for protocols with nonces," in *CSF*. IEEE Computer Society, 2015, pp. 170–184.

[14] V. Cheval, H. Comon-Lundh, and S. Delaune, "A procedure for deciding symbolic equivalence between sets of constraint systems," *Inf. Comput.*, vol. 255, pp. 94–125, 2017.

[15] H. Comon-Lundh, V. Cortier, and G. Scerri, "Tractable inference systems: An extension with a deducibility predicate," in *CADE*, ser. LNCS, vol. 7898. Springer, 2013, pp. 91–108.

[16] M. Abadi and P. Rogaway, "Reconciling two views of cryptography (the computational soundness of formal encryption)," *J. Cryptology*, vol. 15, no. 2, pp. 103–127, 2002.

[17] M. Backes, A. Malik, and D. Unruh, "Computational soundness without protocol restrictions," in *ACM Conference on Computer and Communications Security*. ACM, 2012, pp. 699–711.

[18] M. Backes, E. Mohammadi, and T. Ruffing, "Computational soundness results for prover-if - bridging the gap from trace properties to uniformity," in *POST*, ser. Lecture Notes in Computer Science, vol. 8414. Springer, 2014, pp. 42–62.

[19] M. Bellare, A. Desai, D. Pointcheval, and P. Rogaway, "Relations among notions of security for public-key encryption schemes," in *CRYPTO*, ser. LNCS, vol. 1462. Springer, 1998, pp. 26–45.

[20] V. Shoup, "Sequences of games: a tool for taming complexity in security proofs," *IACR Cryptology ePrint Archive*, vol. 2004, p. 332, 2004, https://eprint.iacr.org/2004/332.

[21] M. Bellare and P. Rogaway, "The security of triple encryption and a framework for code-based game-playing proofs," in *EUROCRYPT*, ser. LNCS, vol. 4004. Springer, 2006, pp. 409–426.

[22] H. Comon and A. Koutsos, "Formal computational unlinkability proofs of RFID protocols," in *30th Computer Security Foundations Symposium, 2017*. IEEE Computer Society, 2017, pp. 100–114.

[23] G. Scerri and R. Stanley-Oakes, "Analysis of key wrapping APIs: Generic policies, computational security," in *IEEE 29th Computer Security Foundations Symposium, CSF 2016, Lisbon, Portugal, June 27 - July 1, 2016*. IEEE Computer Society, 2016, pp. 281–295.

[24] G. Bana, R. Chadha, and A. K. Eeralla, "Formal analysis of vote privacy using computationally complete symbolic attacker," in *ESORICS (2)*, ser. LNCS, vol. 11099. Springer, 2018, pp. 350–372.

[25] A. Koutsos, "Deciding indistinguishability," *CoRR*, vol. abs/1811.06936, 2018.

[26] C. Chang and R. C. T. Lee, *Symbolic logic and mechanical theorem proving*, ser. Computer science classics. Academic Press, 1973.

[27] G. Bana and R. Chadha, "Verification methods for the computationally complete symbolic attacker based on indistinguishability," *IACR Cryptology ePrint Archive*, vol. 2016, p. 69, 2016. [Online]. Available: http://eprint.iacr.org/2016/069

[28] G. Lowe, "An attack on the Needham-Schroeder public-key authentication protocol," *Inf. Process. Lett.*, vol. 56, no. 3, pp. 131–133, 1995.

[29] G. Barthe, J. M. Crespo, B. Grégoire, C. Kunz, Y. Lakhnech, B. Schmidt, and S. Z. Béguelin, "Fully automated analysis of padding-based encryption in the computational model," in *ACM Conference on Computer and Communications Security*. ACM, 2013, pp. 1247–1260.

[30] C. S. Jutla and A. Roy, "Decision procedures for simulatability," in *ESORICS*, ser. LNCS, vol. 7459. Springer, 2012, pp. 573–590.

[31] R. Canetti, "Universally composable security: A new paradigm for cryptographic protocols," in *FOCS*. IEEE Computer Society, 2001, pp. 136–145.

[32] G. Barthe, M. Daubignard, B. M. Kapron, Y. Lakhnech, and V. Laporte, "On the equality of probabilistic terms," in *Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers*, ser. LNCS, E. M. Clarke and A. Voronkov, Eds., vol. 6355. Springer, 2010, pp. 46–63.