# The Squirrel Prover and its Logic

David Baelde, Stéphanie Delaune, Charlie Jacomme, Adrien Koutsos, Joseph Lallemand

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

## To cite this version:

David Baelde, Stéphanie Delaune, Charlie Jacomme, Adrien Koutsos, Joseph Lallemand. The Squirrel Prover and its Logic. ACM SIGLOG News, 2024, 11 (2), 10.1145/3665453.3665461. hal-04579038

HAL Id: hal-04579038

https://inria.hal.science/hal-04579038

Submitted on 17 May 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_2.png" /></figure>
# The Squirrel Prover and its Logic

David Baelde, Stéphanie Delaune, Charlie Jacomme, Adrien Koutsos, Joseph Lallemand

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

## To cite this version:

David Baelde, Stéphanie Delaune, Charlie Jacomme, Adrien Koutsos, Joseph Lallemand. The Squirrel Prover and its Logic. ACM SIGLOG News, 2024, 11 (2), 10.1145/3665453.3665461. hal-04579038

HAL Id: hal-04579038

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

Submitted on 17 May 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_2.png" /></figure>
# The Squirrel Prover and its Logic

David Baelde, Univ Rennes, CNRS, IRISA

Stéphanie Delaune, CNRS, Univ Rennes, IRISA

Charlie Jacomme, Université de Lorraine, LORIA, Inria Nancy Grand-Est

Adrien Koutsos, Inria Paris

Joseph Lallemand, CNRS, Univ Rennes, IRISA

The Squirrel system [Baelde et al. 2021] is an interactive prover for the verification of cryptographic protocols. It relies on a dedicated higher-order logic and provides security guarantees akin to those classically obtained by cryptographers, against attackers modeled as arbitrary probabilistic polynomial-time Turing machines. In this paper, we provide a high-level introduction to the logic behind Squirrel, and briefly describe some of the interesting technical challenges encountered during its construction.

## 1. INTRODUCTION

Security protocols are widely used today to secure transactions that take place over public channels like the Internet. Common uses include the secure transfer of sensitive information such as credit card numbers, or user authentication on a system. Because of their presence in many widely used applications (e.g. electronic commerce, government-issued ID), developing methods and tools to verify security protocols has become an important research challenge. Such tools help increase our trust in protocols, and hence on the applications that rely on them.

Formal methods have brought various approaches to prove that cryptographic protocols indeed guarantee the expected security properties. An effective approach in this area of research consists in modeling cryptographic messages as first-order terms, together with an equational theory that represents attacker capabilities. This idea, originally proposed in [Dolev and Yao 1981], has been refined over the years, resulting in a variety of so-called *symbolic models*. These models encompass broad categories of attackers and facilitate the automated verification of protocols. They have led to the development of successful tools such as ProVerif [Blanchet 2001] and Tamarin [Meier et al. 2013]. However, it is important to note that security in a symbolic model does not necessarily imply security in the cryptographers' standard model, called the *computational model*. In that model, attackers are represented by probabilistic polynomial-time Turing machines (PPTMs), and one proves that a protocol is indistinguishable from an idealized, obviously secure version of it. Verification techniques for the computational model, though crucially needed, often exhibit less flexibility or automation compared to ones for symbolic models. As an illustration, secret keys are faithfully modeled in the computational model as long bitstrings that are drawn uniformly at random, whereas they are modeled using abstract names in symbolic models. In symbolic models, two distinct secret keys are represented by different names, which cannot be equal. However, in the computational model, as in reality, it is possible (although unlikely) that the sampled bitstrings are equal. In this column, we present a recent logic-based method for verifying cryptographic protocols in the computational model, and some practical aspects of its implementation in the Squirrel tool [Baelde et al. 2021; Baelde et al. 2023]. This system is built on the Computationally Complete Symbolic Attacker (CCSA) approach of [Bana and Comon-Lundh 2012; Bana and Comon-Lundh 2014], which relies on the symbolic setting of logic, but avoids the limitations of the symbolic models mentioned above. Instead of modeling attacker capabilities by rules stating what the adversary can do, the CCSA method relies on the specification of what the attacker *cannot* do. Starting from the security properties of cryptographic primitives, one derives rules that articulate which pairs of message sequences are indistinguishable. These
# The Squirrel Prover and its Logic

David Baelde, Univ Rennes, CNRS, IRISA

Stéphanie Delaune, CNRS, Univ Rennes, IRISA

Charlie Jacomme, Université de Lorraine, LORIA, Inria Nancy Grand-Est

Adrien Koutsos, Inria Paris

Joseph Lallemand, CNRS, Univ Rennes, IRISA

The Squirrel system [Baelde et al. 2021] is an interactive prover for the verification of cryptographic protocols. It relies on a dedicated higher-order logic and provides security guarantees akin to those classically obtained by cryptographers, against attackers modeled as arbitrary probabilistic polynomial-time Turing machines. In this paper, we provide a high-level introduction to the logic behind Squirrel, and briefly describe some of the interesting technical challenges encountered during its construction.

## 1. INTRODUCTION

Security protocols are widely used today to secure transactions that take place over public channels like the Internet. Common uses include the secure transfer of sensitive information such as credit card numbers, or user authentication on a system. Because of their presence in many widely used applications (e.g. electronic commerce, government-issued ID), developing methods and tools to verify security protocols has become an important research challenge. Such tools help increase our trust in protocols, and hence on the applications that rely on them.

Formal methods have brought various approaches to prove that cryptographic protocols indeed guarantee the expected security properties. An effective approach in this area of research consists in modeling cryptographic messages as first-order terms, together with an equational theory that represents attacker capabilities. This idea, originally proposed in [Dolev and Yao 1981], has been refined over the years, resulting in a variety of so-called *symbolic models*. These models encompass broad categories of attackers and facilitate the automated verification of protocols. They have led to the development of successful tools such as ProVerif [Blanchet 2001] and Tamarin [Meier et al. 2013]. However, it is important to note that security in a symbolic model does not necessarily imply security in the cryptographers' standard model, called the *computational model*. In that model, attackers are represented by probabilistic polynomial-time Turing machines (PPTMs), and one proves that a protocol is indistinguishable from an idealized, obviously secure version of it. Verification techniques for the computational model, though crucially needed, often exhibit less flexibility or automation compared to ones for symbolic models. As an illustration, secret keys are faithfully modeled in the computational model as long bitstrings that are drawn uniformly at random, whereas they are modeled using abstract names in symbolic models. In symbolic models, two distinct secret keys are represented by different names, which cannot be equal. However, in the computational model, as in reality, it is possible (although unlikely) that the sampled bitstrings are equal. In this column, we present a recent logic-based method for verifying cryptographic protocols in the computational model, and some practical aspects of its implementation in the Squirrel tool [Baelde et al. 2021; Baelde et al. 2023]. This system is built on the Computationally Complete Symbolic Attacker (CCSA) approach of [Bana and Comon-Lundh 2012; Bana and Comon-Lundh 2014], which relies on the symbolic setting of logic, but avoids the limitations of the symbolic models mentioned above. Instead of modeling attacker capabilities by rules stating what the adversary can do, the CCSA method relies on the specification of what the attacker *cannot* do. Starting from the security properties of cryptographic primitives, one derives rules that articulate which pairs of message sequences are indistinguishable. These
rules are proved sound w.r.t. the interpretation of terms as PPTMs. Therefore, a proof of a security property using these rules implies security in the computational model under the initial cryptographic assumptions. The CCSA logic was later extended into a meta-logic, which served as basis for the first version of Squirrel [Baelde et al. 2021], before being generalized to a fully-fledged higher-order logic in [Baelde et al. 2023]. The Squirrel tool is a proof assistant developed in a collaborative effort, which has been successfully used on a variety of case studies [Baelde et al. 2022; Comon et al. 2020; Cremers et al. 2022]. Instructions for installing the system are available on its website, together with a user manual, tutorials, and an in-browser interface for playing with the tool without installing it:

https://squirrel-prover.github.io

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

We first provide, in Section 2, an introduction to the computational model and the CCSA approach, showing in particular how cryptographic assumptions translate into logical rules. We elaborate on this in Section 3 to show how protocols can be modeled in CCSA logic, discussing a subtle issue w.r.t. the intended notion of security. Finally, Section 4 formally defines the higher-order CCSA logic, on which Squirrel is based, and discusses some of its interesting technical features: the distinction between local and global formulas, the subtleties tied to reasoning about probabilistic objects, and the key notion of bi-deduction for reasoning about computational indistinguishability.

*Related work.* Squirrel is only a recent addition to the list of available systems for verifying cryptographic protocols. We have mentioned above some tools that provide guarantees in symbolic models; we now briefly present the tools providing guarantees in the computational model. Several such systems exist, based on different approaches. The earliest one is CryptoVerif [Blanchet 2008], which mechanizes proofs based on high-level game transformations, following the style of pen-and-paper proofs. The most prominent system today is probably EasyCrypt [Barthe et al. 2011], which is a proof assistant also featuring higher-order logic. It notably embeds a domain-specific probabilistic relational Hoare logic [Barthe et al. 2009], which can capture cryptographic game transformations. This design makes it possible to carry out most cryptographic arguments within EasyCrypt. Other systems are currently being developed, with various goals: notably CryptHOL [Basin et al. 2020], which explores an alternative modeling technique in Isabelle/HOL, and F\* [Swamy et al. 2016], which is a general-purpose program verification framework based on refinement types that can be used (via external arguments) to provide computational security guarantees. Those approaches can be compared on several criteria [Barbosa et al. 2021].

Here, we only compare with the closest two tools, and only with respect to three criteria, to highlight differences: modeling, automation, and proof methodology. Regarding modeling, CryptoVerif and Squirrel have a similar level of detail and expressivity, although CryptoVerif supports a larger range of cryptographic assumptions. EasyCrypt is more expressive, with a higher level of detail, at the cost of modeling overhead, and thus better suited for proving properties of primitives. Protocol specifications in CryptoVerif and Squirrel are given in a process algebra, whereas protocols are encoded in EasyCrypt as APIs, which is inconvenient for interactive protocols. Finally, CryptoVerif does not support stateful protocols, while Squirrel and EasyCrypt do.

Overall, the current level of automation of Squirrel sits somewhere between CryptoVerif, which can apply cryptographic arguments automatically, although it often requires hints about which game transformations to use, and EasyCrypt, which does not automatically apply cryptographic arguments.
rules are proved sound w.r.t. the interpretation of terms as PPTMs. Therefore, a proof of a security property using these rules implies security in the computational model under the initial cryptographic assumptions. The CCSA logic was later extended into a meta-logic, which served as basis for the first version of Squirrel [Baelde et al. 2021], before being generalized to a fully-fledged higher-order logic in [Baelde et al. 2023]. The Squirrel tool is a proof assistant developed in a collaborative effort, which has been successfully used on a variety of case studies [Baelde et al. 2022; Comon et al. 2020; Cremers et al. 2022]. Instructions for installing the system are available on its website, together with a user manual, tutorials, and an in-browser interface for playing with the tool without installing it:

https://squirrel-prover.github.io

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

We first provide, in Section 2, an introduction to the computational model and the CCSA approach, showing in particular how cryptographic assumptions translate into logical rules. We elaborate on this in Section 3 to show how protocols can be modeled in CCSA logic, discussing a subtle issue w.r.t. the intended notion of security. Finally, Section 4 formally defines the higher-order CCSA logic, on which Squirrel is based, and discusses some of its interesting technical features: the distinction between local and global formulas, the subtleties tied to reasoning about probabilistic objects, and the key notion of bi-deduction for reasoning about computational indistinguishability.

*Related work.* Squirrel is only a recent addition to the list of available systems for verifying cryptographic protocols. We have mentioned above some tools that provide guarantees in symbolic models; we now briefly present the tools providing guarantees in the computational model. Several such systems exist, based on different approaches. The earliest one is CryptoVerif [Blanchet 2008], which mechanizes proofs based on high-level game transformations, following the style of pen-and-paper proofs. The most prominent system today is probably EasyCrypt [Barthe et al. 2011], which is a proof assistant also featuring higher-order logic. It notably embeds a domain-specific probabilistic relational Hoare logic [Barthe et al. 2009], which can capture cryptographic game transformations. This design makes it possible to carry out most cryptographic arguments within EasyCrypt. Other systems are currently being developed, with various goals: notably CryptHOL [Basin et al. 2020], which explores an alternative modeling technique in Isabelle/HOL, and F\* [Swamy et al. 2016], which is a general-purpose program verification framework based on refinement types that can be used (via external arguments) to provide computational security guarantees. Those approaches can be compared on several criteria [Barbosa et al. 2021].

Here, we only compare with the closest two tools, and only with respect to three criteria, to highlight differences: modeling, automation, and proof methodology. Regarding modeling, CryptoVerif and Squirrel have a similar level of detail and expressivity, although CryptoVerif supports a larger range of cryptographic assumptions. EasyCrypt is more expressive, with a higher level of detail, at the cost of modeling overhead, and thus better suited for proving properties of primitives. Protocol specifications in CryptoVerif and Squirrel are given in a process algebra, whereas protocols are encoded in EasyCrypt as APIs, which is inconvenient for interactive protocols. Finally, CryptoVerif does not support stateful protocols, while Squirrel and EasyCrypt do.

Overall, the current level of automation of Squirrel sits somewhere between CryptoVerif, which can apply cryptographic arguments automatically, although it often requires hints about which game transformations to use, and EasyCrypt, which does not automatically apply cryptographic arguments.
Finally, the most important difference between Squirrel and the other tools is the associated proof methodology: CryptoVerif relies on game transformations and EasyCrypt performs Hoare-style proofs of programs, while Squirrel reasons over execution traces of protocols.

## 2. A BASIC INDISTINGUISHABILITY LOGIC

We introduce in this section the CCSA approach, which is designed to reason on cryptographic protocols, i.e. concurrent programs relying on cryptographic primitives to achieve some functionality while running in a malicious environment. To simplify our exposition, we delay the treatment of general protocols to Section 3, and restrict our presentation to simple sequential cryptographic games for the time being. These games are used by cryptographers to express security properties of cryptographic primitives against attackers modeled as arbitrary polynomial-time computations. A key concept about games is computational indistinguishability: roughly, two games are indistinguishable if any polynomial-time adversary has at-best a negligible probability in distinguishing them. In the CCSA approach, we use first-order logic to establish computational indistinguishability: we first model the messages derived during a game's execution as first-order terms, and then reason about computational indistinguishability in first-order logic, using inference rules derived from cryptographic assumptions.

A key aspect of the logic is that it abstracts cryptographic arguments as much as possible. Notably, its syntax does not mention the length of keys or the value of probabilities. Further, reduction-based arguments are implicit: they justify the soundness of the proof rules, but the code underlying reductions is never explicitly stated.

### 2.1. The core of the logic

Security in the real world is often conditional, as there is usually a small but non-zero probability that the adversary manages to break the security of a system. Typically, one cannot rule out that a lucky attacker guesses a secret key. To discard such unlikely cases, security is considered up to a negligible probability of attack. A function $f: \mathbb{N} \to [0, 1]$ is negligible if it is asymptotically lower than the inverse of any polynomial, i.e. if $\forall k \in \mathbb{N}. \exists n_0. \forall n \ge n_0. f(n) \le \frac{1}{n^k}$. Conversely, $f$ is overwhelming if $1 - f$ is negligible. In what follows, we will thus use a security parameter $\eta \in \mathbb{N}$ which can be, e.g., the length of the secret keys, and security must hold with overwhelming probability w.r.t. $\eta$.

In the cryptographic literature, security properties are commonly specified using so-called *games*, in which an adversary tries to mount an attack: the game might represent an adversary attempting to guess a secret value, to forge a signature, ... Games are usually written in pseudo-code using an imperative style, as shown in Figure 1. The statement $x \Leftarrow D$ stores the result of a random sampling following distribution $D$ into variable $x$: e.g. $sk \Leftarrow \{0, 1\}^\eta$ uniformly samples a secret key sk of $\eta$ bits. Games are parameterized by an abstract *interactive attacker*, denoted by $\mathcal{A}$. The statement $o \leftarrow \mathcal{A}(i)$ calls the adversary $\mathcal{A}$ on input $i$, and stores its answer in variable $o$. The adversary is stateful, retaining information across its invocations. Standard assignments are denoted in the same way: $x \leftarrow e$ stores the result of evaluating $e$ into variable $x$.

Describing cryptographic games as probabilistic imperative programs lets cryptographers rely on the reader's intuitive understanding of their semantics, and avoids introducing convoluted execution models. However, this comes at a cost: formally reasoning over such programs can be difficult (one needs to deal with statefulness, loop invariants, probabilistic dependencies, ...); moreover, encoding complex protocols as imperative programs is possible but not natural, and complicates security proofs.
Finally, the most important difference between Squirrel and the other tools is the as-
sociated proof methodology: CryptoVerif relies on game transformations and EasyCrypt
performs Hoare-style proofs of programs, while Squirrel reasons over execution traces
of protocols.

## 2. A BASIC INDISTINGUISHABILITY LOGIC

We introduce in this section the CCSA approach, which is designed to reason on cryp-
tographic protocols, i.e. concurrent programs relying on cryptographic primitives to
achieve some functionality while running in a malicious environment. To simplify
our exposition, we delay the treatment of general protocols to Section 3, and restrict
our presentation to simple sequential cryptographic games for the time being. These
games are used by cryptographers to express security properties of cryptographic prim-
itives against attackers modeled as arbitrary polynomial-time computations. A key
concept about games is computational indistinguishability: roughly, two games are
indistinguishable if any polynomial-time adversary has at-best a negligible probability
in distinguishing them. In the CCSA approach, we use first-order logic to establish com-
putational indistinguishability: we first model the messages derived during a game's
execution as first-order terms, and then reason about computational indistinguishability
in first-order logic, using inference rules derived from cryptographic assumptions.

A key aspect of the logic is that it abstracts cryptographic arguments as much
as possible. Notably, its syntax does not mention the length of keys or the value
of probabilities. Further, reduction-based arguments are implicit: they justify the
soundness of the proof rules, but the code underlying reductions is never explicitly
stated.

2.1. The core of the logic

Security in the real world is often conditional, as there is usually a small but non-zero
probability that the adversary manages to break the security of a system. Typically, one
cannot rule out that a lucky attacker guesses a secret key. To discard such unlikely cases,
security is considered up to a *negligible* probability of attack. A function $f : \mathbb{N} \to [0, 1]$ is *negligible* if it is asymptotically lower than the inverse of any polynomial, i.e. if
$\forall k \in \mathbb{N}. \exists n_0. \forall n \ge n_0. f(n) \le \frac{1}{n^k}$. Conversely, $f$ is *overwhelming* if $1 - f$ is negligible. In
what follows, we will thus use a *security parameter* $\eta \in \mathbb{N}$ which can be, e.g., the length
of the secret keys, and security must hold with *overwhelming* probability w.r.t. $\eta$.

In the cryptographic literature, security properties are commonly specified using so-
called *games*, in which an adversary tries to mount an attack: the game might represent
an adversary attempting to guess a secret value, to forge a signature, ... Games are
usually written in pseudo-code using an imperative style, as shown in Figure 1. The
statement $x \Leftarrow D$ stores the result of a random sampling following distribution $D$
into variable $x$: e.g. $sk \Leftarrow \{0, 1\}^\eta$ uniformly samples a secret key sk of $\eta$ bits. Games are
parameterized by an abstract *interactive attacker*, denoted by $\mathcal{A}$. The statement $o \Leftarrow \mathcal{A}(i)$
calls the adversary $\mathcal{A}$ on input $i$, and stores its answer in variable $o$. The adversary
is stateful, retaining information across its invocations. Standard assignments are
denoted in the same way: $x \leftarrow e$ stores the result of evaluating $e$ into variable $x$.

Describing cryptographic games as probabilistic imperative programs lets cryptog-
raphers rely on the reader's intuitive understanding of their semantics, and avoids
introducing convoluted execution models. However, this comes at a cost: formally rea-
soning over such programs can be difficult (one needs to deal with statefulness, loop
invariants, probabilistic dependencies, ...); moreover, encoding complex protocols as
imperative programs is possible but not natural, and complicates security proofs.
Game $\mathcal{G}$:

1: sk $\leftarrow^S \{0, 1\}^\eta$;

2: $m \leftarrow A$;

3: $t \leftarrow \text{enc}(m, sk)$;

4: $x \leftarrow A(t)$;

5: return $x$

A secret key sk of length $\eta$ is randomly sampled. The interactive attacker $\mathcal{A}$ is asked to provide a message $m$ which is then encrypted (using sk) and sent back to $\mathcal{A}$. Afterwards, $\mathcal{A}$ returns a second message $x$ which is the final output of the game.

<caption>Fig. 1. An example cryptographic game.</caption>

*Cryptographic games in CCSA.* In the CCSA approach, we do not explicitly represent games. Instead, we shall only represent the messages computed at different points in a game, using first-order terms. Those are pure, unlike the stateful games, and thus easier to reason about. Our terms are built using:

- honest function symbols which represent the various primitives used to compute messages (e.g. pairing, encryption);

- attacker function symbols, noted $\text{att}_i$ for $i \in \mathbb{N}$, modeling arbitrary computations performed by adversaries;

- name symbols, representing the sources of randomness: essentially, a name is a pointer to a memory cell holding a value sampled at random before the game starts.

**Example 2.1.** Let us illustrate this approach by modeling the final result of the game of Figure 1 as a single term. The sampling of the secret key is modeled by a name symbol sk. The first call to the attacker $A$() is modeled by the term $\text{att}_0()$. In the imperative game modeling style, internal functions (e.g. the encryption enc) can be probabilistic, but this is not so in our approach, where we precisely track probabilistic dependencies. Thus, we explicitly specify the randomness used by the encryption function enc, by introducing a name symbol r and using the term $\text{enc}(\text{att}_0(), r, sk)$ to model $t$ in the game. Then, the second call to the adversary can be modeled using a different adversarial function symbol, as: $\text{att}_1(\text{enc}(\text{att}_0(), r, sk))$. Importantly, we have modeled two successive calls to the stateful attacker $\mathcal{A}$ in the game by two pure functions ($\text{att}_0$ and $\text{att}_1$). This is without loss of generality, as any state computed during the first call to $\mathcal{A}$ and used in the second call can be recomputed when modeling the second call as $\text{att}_1$.

*Models of the logic.* Defining the logic's semantics in order to have a faithful translation from games to terms requires a bit of care. The interpretation of a term is parameterized by the security parameter $\eta \in \mathbb{N}$, as well as two explicit sources of randomness provided by a pair $\rho = (\rho_h, \rho_a)$ of tapes filled with random bits. A model $\mathcal{M}$ of our logic must:

- provide for each honest function symbol $f$ its interpretation as a PPTM $M_f$;

- associate to each name $n$ a unique sub-sequence of $\eta$ bits in $\rho_h$ using a PPTM $M_n$ with access to $\rho_h$, such that distinct names use disjoint parts of $\rho_h$;

- interpret any adversarial function symbol $\text{att}$ as a PPTM $M_{\text{att}}$ which can only access the random tape $\rho_a$ (but not $\rho_h$).

For the sake of simplicity, we forced names to be interpreted as uniform and independent random samplings in $\{0, 1\}^\eta$.

Our models are first-order models with a tailored interpretation domain. Thus, terms can be interpreted in $\mathcal{M}$ using the standard semantics of first-order logic. In our specific setting, a term $t$ is interpreted as a function associating, to each value of the security parameter $\eta$ and random tapes $\rho$, the interpretation $\llbracket t \rrbracket_{\mathcal{M}}^{\eta, \rho}$. More precisely, the function $\eta, \rho \mapsto \llbracket t \rrbracket_{\mathcal{M}}^{\eta, \rho}$ is computed by a PPTM.
Game $\mathcal{G}$:

1: sk $\leftarrow^S \{0, 1\}^\eta$;

2: $m \leftarrow A$;

3: $t \leftarrow \text{enc}(m, sk)$;

4: $x \leftarrow A(t)$;

5: return $x$

A secret key sk of length $\eta$ is randomly sampled. The interactive attacker $\mathcal{A}$ is asked to provide a message $m$ which is then encrypted (using sk) and sent back to $\mathcal{A}$. Afterwards, $\mathcal{A}$ returns a second message $x$ which is the final output of the game.

<caption>Fig. 1. An example cryptographic game.</caption>

*Cryptographic games in CCSA.* In the CCSA approach, we do not explicitly represent games. Instead, we shall only represent the messages computed at different points in a game, using first-order terms. Those are pure, unlike the stateful games, and thus easier to reason about. Our terms are built using:

- honest function symbols which represent the various primitives used to compute messages (e.g. pairing, encryption);

- attacker function symbols, noted $\text{att}_i$ for $i \in \mathbb{N}$, modeling arbitrary computations performed by adversaries;

- name symbols, representing the sources of randomness: essentially, a name is a pointer to a memory cell holding a value sampled at random before the game starts.

*Example 2.1.* Let us illustrate this approach by modeling the final result of the game of Figure 1 as a single term. The sampling of the secret key is modeled by a name symbol sk. The first call to the attacker $A$() is modeled by the term $\text{att}_0()$. In the imperative game modeling style, internal functions (e.g. the encryption enc) can be probabilistic, but this is not so in our approach, where we precisely track probabilistic dependencies. Thus, we explicitly specify the randomness used by the encryption function enc, by introducing a name symbol r and using the term $\text{enc}(\text{att}_0(), r, sk)$ to model $t$ in the game. Then, the second call to the adversary can be modeled using a different adversarial function symbol, as: $\text{att}_1(\text{enc}(\text{att}_0(), r, sk))$. Importantly, we have modeled two successive calls to the stateful attacker $\mathcal{A}$ in the game by two pure functions ($\text{att}_0$ and $\text{att}_1$). This is without loss of generality, as any state computed during the first call to $\mathcal{A}$ and used in the second call can be recomputed when modeling the second call as $\text{att}_1$.

*Models of the logic.* Defining the logic's semantics in order to have a faithful translation from games to terms requires a bit of care. The interpretation of a term is parameterized by the security parameter $\eta \in \mathbb{N}$, as well as two explicit sources of randomness provided by a pair $\rho = (\rho_h, \rho_a)$ of tapes filled with random bits. A model $\mathcal{M}$ of our logic must:

- provide for each honest function symbol $f$ its interpretation as a PPTM $M_f$;

- associate to each name $n$ a unique sub-sequence of $\eta$ bits in $\rho_h$ using a PPTM $M_n$ with access to $\rho_h$, such that distinct names use disjoint parts of $\rho_h$;

- interpret any adversarial function symbol $\text{att}$ as a PPTM $M_{\text{att}}$ which can only access the random tape $\rho_a$ (but not $\rho_h$).

For the sake of simplicity, we forced names to be interpreted as uniform and independent random samplings in $\{0, 1\}^\eta$.

Our models are first-order models with a tailored interpretation domain. Thus, terms can be interpreted in $\mathcal{M}$ using the standard semantics of first-order logic. In our specific setting, a term $t$ is interpreted as a function associating, to each value of the security parameter $\eta$ and random tapes $\rho$, the interpretation $\llbracket t \rrbracket_{\mathcal{M}}^{\eta, \rho}$. More precisely, the function $\eta, \rho \mapsto \llbracket t \rrbracket_{\mathcal{M}}^{\eta, \rho}$ is computed by a PPTM.
For example, the interpretation $\llbracket n \rrbracket_M^{\eta, \rho}$ of a name symbol n is computed by $M_n(\eta, \rho_h)$, and an adversarial computation is computed by $\llbracket \text{att}_i(t) \rrbracket_M^{\eta, \rho} = M_{\text{att}_i}(\eta, \llbracket t \rrbracket_M^{\eta, \rho}, \rho_a)$. Importantly, this interpretation is compositional and makes all probability dependencies explicit, which will facilitate reasoning over cryptographic messages.

*Example 2.2.* Coming back to $\mathcal{G}$ from Figure 1, the value in the variable $x$ at the end of $\mathcal{G}$'s execution follows the same probability distribution as

$$ \llbracket \text{att}_1(\text{enc}(\text{att}_0(), r, sk)) \rrbracket_M^{\eta, \rho} $$

where the tapes in $\rho$ are sampled at random, and where $M$ interprets the encryption and attacker functions as does $\mathcal{G}$.

Using Turing machines to interpret terms gives us a high level of expressivity. For instance, conditional branching in games can be internalized in the first-order terms using an (if $b$ then $t$ else $e$) function symbol whose interpretation is forced to be the natural one in all models.

*Example 2.3.* Consider the following game:

Game $\mathcal{G}_{sk}$

1: sk $\leftarrow^s \{0, 1\}^\eta$;

2: $m \leftarrow \mathcal{A}$;

3: if $m = sk$ then

4: return 0

5: else

6: return 1

This game samples a fresh secret key and queries the attacker to obtain a guess $m$ for the key. The game outputs 0 if the attacker correctly guessed the key, and 1 otherwise. The message returned at the end of the game can be represented by the following term:

$$ \phi_{sk} \stackrel{\text{def}}{=} \text{if } (\text{att}_0() = sk) \text{ then } 0 \text{ else } 1. $$

## 2.2. The computational indistinguishability predicate $\sim$

One of the most commonly used notions to define cryptographic properties is computational indistinguishability. Roughly, indistinguishability is expressed as a guessing game in which an adversary must figure out which one of two scenarios $\mathcal{G}_I$ or $\mathcal{G}_R$ it is interacting with. More precisely, two games $\mathcal{G}_I$ and $\mathcal{G}_R$ are indistinguishable, which we write $\mathcal{G}_I \approx \mathcal{G}_R$, when any PPTM adversary has at-best a negligible probability of guessing whether it is interacting with $\mathcal{G}_I$ or $\mathcal{G}_R$. Formally, we define the advantage of the attacker $\mathcal{A}$ as the probability that it makes the two games behave differently. We then require this advantage to be negligible in the security parameter $\eta$:

$$ \forall \mathcal{A} \in \text{PPTM.} \quad \eta \mapsto |\text{Pr}(\mathcal{G}_I(\mathcal{A}) = 1) - \text{Pr}(\mathcal{G}_R(\mathcal{A}) = 1)| \text{ is negligible.} $$

Typically, the game $\mathcal{G}_R$ will correspond to an attack against the real primitives, while $\mathcal{G}_I$ will represent an attack against an idealized implementation of the primitives for which security is obvious.

*Example 2.4.* Coming back to Example 2.3, the indistinguishability $\mathcal{G}_{sk} \approx (\text{return } 1)$ states that the probability that the adversary $\mathcal{A}$ guesses the secret key sk is negligible. In that case, a simple probabilistic independence argument can be used to show that the probability that $\mathcal{A}$ computes sk is $\frac{1}{2^\eta}$. Thus, the indistinguishability holds.

Squirrel's logic relies on a predicate $\sim$ to represent computational indistinguishability. Formally, for two terms $u, v$, the predicate $u \sim v$ holds in a model $M$ if $\mathcal{G}_u^M \approx \mathcal{G}_v^M$, where $\mathcal{G}_t^M$ is the game where the adversary is provided with $\llbracket t \rrbracket_M^{\eta, \rho}$ and must produce a bit $b$, which the game returns. In other words, $u \sim v$ in $M$ when:

$$ \forall \mathcal{A} \in \text{PPTM.} \quad \eta \mapsto |\text{Pr}_{\rho}(\mathcal{A}(\llbracket u \rrbracket_M^{\eta, \rho}, \rho_a) = 1) - \text{Pr}_{\rho}(\mathcal{A}(\llbracket v \rrbracket_M^{\eta, \rho}, \rho_a) = 1)| \text{ is negligible.} $$
For example, the interpretation $\llbracket n \rrbracket_M^{\eta;\rho}$ of a name symbol n is computed by $M_n(\eta, \rho_h)$, and an adversarial computation is computed by $\llbracket \text{att}_i(t) \rrbracket_M^{\eta;\rho} = M_{\text{att}_i}(\eta, \llbracket t \rrbracket_M^{\eta;\rho}, \rho_a)$. Importantly, this interpretation is compositional and makes all probability dependencies explicit, which will facilitate reasoning over cryptographic messages.

*Example 2.2.* Coming back to $\mathcal{G}$ from Figure 1, the value in the variable $x$ at the end of $\mathcal{G}$'s execution follows the same probability distribution as

$$ \llbracket \text{att}_1(\text{enc}(\text{att}_0(), r, sk)) \rrbracket_M^{\eta;\rho} $$

where the tapes in $\rho$ are sampled at random, and where $M$ interprets the encryption and attacker functions as does $\mathcal{G}$.

Using Turing machines to interpret terms gives us a high level of expressivity. For instance, conditional branching in games can be internalized in the first-order terms using an (if $b$ then $t$ else $e$) function symbol whose interpretation is forced to be the natural one in all models.

*Example 2.3.* Consider the following game:

Game $\mathcal{G}_{sk}$

1: sk $\leftarrow^s \{0, 1\}^\eta$;

2: $m \leftarrow \mathcal{A}$;

3: if $m = sk$ then

4: return 0

5: else

6: return 1

This game samples a fresh secret key and queries the attacker to obtain a guess $m$ for the key. The game outputs 0 if the attacker correctly guessed the key, and 1 otherwise. The message returned at the end of the game can be represented by the following term:

$$ \phi_{sk} \stackrel{\text{def}}{=} \text{if } (\text{att}_0() = sk) \text{ then } 0 \text{ else } 1. $$

## 2.2. The computational indistinguishability predicate $\sim$

One of the most commonly used notions to define cryptographic properties is computational indistinguishability. Roughly, indistinguishability is expressed as a guessing game in which an adversary must figure out which one of two scenarios $\mathcal{G}_I$ or $\mathcal{G}_R$ it is interacting with. More precisely, two games $\mathcal{G}_I$ and $\mathcal{G}_R$ are indistinguishable, which we write $\mathcal{G}_I \approx \mathcal{G}_R$, when any PPTM adversary has at-best a negligible probability of guessing whether it is interacting with $\mathcal{G}_I$ or $\mathcal{G}_R$. Formally, we define the advantage of the attacker $\mathcal{A}$ as the probability that it makes the two games behave differently. We then require this advantage to be negligible in the security parameter $\eta$:

$$ \forall \mathcal{A} \in \text{PPTM.} \quad \eta \mapsto |\text{Pr}(\mathcal{G}_I(\mathcal{A}) = 1) - \text{Pr}(\mathcal{G}_R(\mathcal{A}) = 1)| \text{ is negligible.} $$

Typically, the game $\mathcal{G}_R$ will correspond to an attack against the real primitives, while $\mathcal{G}_I$ will represent an attack against an idealized implementation of the primitives for which security is obvious.

*Example 2.4.* Coming back to Example 2.3, the indistinguishability $\mathcal{G}_{sk} \approx (\text{return } 1)$ states that the probability that the adversary $\mathcal{A}$ guesses the secret key sk is negligible. In that case, a simple probabilistic independence argument can be used to show that the probability that $\mathcal{A}$ computes sk is $\frac{1}{2^\eta}$. Thus, the indistinguishability holds.

Squirrel's logic relies on a predicate $\sim$ to represent computational indistinguishability. Formally, for two terms $u, v$, the predicate $u \sim v$ holds in a model $M$ if $\mathcal{G}_u^M \approx \mathcal{G}_v^M$, where $\mathcal{G}_t^M$ is the game where the adversary is provided with $\llbracket t \rrbracket_M^{\eta;\rho}$ and must produce a bit $b$, which the game returns. In other words, $u \sim v$ in $M$ when:

$$ \forall \mathcal{A} \in \text{PPTM.} \quad \eta \mapsto |\text{Pr}_{\rho}(\mathcal{A}(\llbracket u \rrbracket_M^{\eta;\rho}, \rho_a) = 1) - \text{Pr}_{\rho}(\mathcal{A}(\llbracket v \rrbracket_M^{\eta;\rho}, \rho_a) = 1)| \text{ is negligible.} $$
<figure><img src="image_4.png" /><figcaption>Fig. 2. Basic inference rules over $\sim$.</figcaption></figure>

**Example 2.5.** Reusing $\mathcal{G}_{sk}$ and $\phi_{sk}$ from Example 2.3, checking $\phi_{sk} \sim 1$ amounts to verifying that $\mathcal{G}_{sk} \approx$ (return 1).

In the example above, we have used the indistinguishability predicate on booleans. In that case, the semantics of $\sim$ can be restated in a simpler way, without a quantification over all distinguishers $A$: it simply means that the two booleans have the same probability of being 1. The general semantics of $\sim$ becomes useful, though, to reason on it by decomposing terms: for instance, it allows us to derive $f(u) \sim f(v)$ from $u \sim v$ for any $u$ and $v$ of arbitrary types. Indeed, the existence of a PPTM distinguishing between $f(u)$ and $f(v)$ implies the existence of a PPTM distinguishing between $u$ and $v$: the latter distinguisher is obtained by composing the former with the PPTM computing $f$.

**Logical rules.** We now present some rules that can be used to reason over $\sim$. We intuitively describe some of those rules here, starting with the simpler rules that do not rely on any security assumptions over the primitives.

**Example 2.6.** The following formulas are valid:

(1) $t \sim t$ for any term $t$; indistinguishability is reflexive.

(2) $n \sim n'$ for any names $n, n'$; two uniform random samplings are indistinguishable.

(3) $(n, n) \not\sim (n, n')$; the attacker sees, in one case, the same value twice, and in the other, two distinct values (with overwhelming probability). Notice that this implies that $\sim$ does not lift to an arbitrary context: we have seen that $n \sim n'$, but this example shows that we do not have for all context $C$ that $C[n] \sim C[n']$.

(4) (if true then $u$ else $v = u$) $\sim$ true for any terms $u, v$; more generally, any term occurring in an indistinguishability can be rewritten into an equal term.

(5) $(n \neq n') \sim$ true; names, i.e. random samplings, collide with negligible probability.

We provide a first set of inference rules in Figure 2. `REFL` corresponds to the reflexivity of $\sim$, and `REWRITE` allows replacing two terms that are equal with overwhelming probability in any context. Finally, `FRESH` exploits the fact that a term syntactically contains all its probabilistic dependencies: if a name $n$ does not occur in a term $t$, then $n$ is a uniform random sampling independent of $t$, and thus $t = n$ can only be true with negligible probability.

**Example 2.7.** Let us go back to Example 2.5 and the formula $\phi_{sk} \sim 1$. We assume an additional proof rule `SIMPL=的是` that allows to replace a term with another one equal to it with probability one, which we note $\equiv$, and where for instance, $v \equiv$ (if false then $u$ else $v$). We can prove our goal with the following derivation:

$$ \begin{array}{c} \begin{array}{c} \text{FRESH} \\ \text{SIMPL=} \end{array} & \begin{array}{c} \overline{(\text{att}_0() \neq \text{sk}) \sim \text{true}} \\ \frac{((\text{att}_0() = \text{sk}) = \text{false}) \sim \text{true}}{\text{SIMPL=}} \end{array} & \begin{array}{c} \text{REFL} \\ \frac{1 \sim 1}{(\text{if false then } 0 \text{ else } 1) \sim 1} \end{array} \\ \text{REWRITE} & & \end{array} $$

Here, we use twice `SIMPL=`: once with the previously mentioned equality over a false conditional, and once using the fact that $((\text{att}_0() = \text{sk}) = \text{false}) \equiv (\text{att}_0() \neq \text{sk})$.
<figure><img src="image_4.png" /><figcaption>Fig. 2. Basic inference rules over $\sim$.</figcaption></figure>

**Example 2.5.** Reusing $\mathcal{G}_{sk}$ and $\phi_{sk}$ from Example 2.3, checking $\phi_{sk} \sim 1$ amounts to verifying that $\mathcal{G}_{sk} \approx (\text{return } 1)$.

In the example above, we have used the indistinguishability predicate on booleans. In that case, the semantics of $\sim$ can be restated in a simpler way, without a quantification over all distinguishers $A$: it simply means that the two booleans have the same probability of being 1. The general semantics of $\sim$ becomes useful, though, to reason on it by decomposing terms: for instance, it allows us to derive $f(u) \sim f(v)$ from $u \sim v$ for any $u$ and $v$ of arbitrary types. Indeed, the existence of a PPTM distinguishing between $f(u)$ and $f(v)$ implies the existence of a PPTM distinguishing between $u$ and $v$: the latter distinguisher is obtained by composing the former with the PPTM computing $f$.

**Logical rules.** We now present some rules that can be used to reason over $\sim$. We intuitively describe some of those rules here, starting with the simpler rules that do not rely on any security assumptions over the primitives.

**Example 2.6.** The following formulas are valid:

(1) $t \sim t$ for any term $t$; indistinguishability is reflexive.

(2) $n \sim n'$ for any names $n, n'$; two uniform random samplings are indistinguishable.

(3) $(n, n) \not\sim (n, n')$; the attacker sees, in one case, the same value twice, and in the other, two distinct values (with overwhelming probability). Notice that this implies that $\sim$ does not lift to an arbitrary context: we have seen that $n \sim n'$, but this example shows that we do not have for all context $C$ that $C[n] \sim C[n']$.

(4) (if true then $u$ else $v = u$) $\sim$ true for any terms $u, v$; more generally, any term occurring in an indistinguishability can be rewritten into an equal term.

(5) $(n \neq n') \sim$ true; names, i.e. random samplings, collide with negligible probability.

We provide a first set of inference rules in Figure 2. `REFL` corresponds to the reflexivity of $\sim$, and `REWRITE` allows replacing two terms that are equal with overwhelming probability in any context. Finally, `FRESH` exploits the fact that a term syntactically contains all its probabilistic dependencies: if a name $n$ does not occur in a term $t$, then $n$ is a uniform random sampling independent of $t$, and thus $t = n$ can only be true with negligible probability.

**Example 2.7.** Let us go back to Example 2.5 and the formula $\phi_{sk} \sim 1$. We assume an additional proof rule `SIMPL=:` that allows to replace a term with another one equal to it with probability one, which we note $=$, and where for instance, $v = \text{(if false then } u \text{ else } v)$. We can prove our goal with the following derivation:

$$ \begin{array}{c} \begin{array}{c} \text{FRESH} \\ \text{SIMPL=}: \\ \text{REWRITE} \end{array} \\ \frac{\overline{(\text{att}_0() \neq \text{sk}) \sim \text{true}}}{((\text{att}_0() = \text{sk}) = \text{false}) \sim \text{true}} \quad \text{SIMPL=} \quad \frac{\overline{(\text{if false then } 0 \text{ else } 1) \sim 1}}{(\text{if att}_0() = \text{sk} \text{ then } 0 \text{ else } 1) \sim 1} \end{array} $$

Here, we use twice `SIMPL=:` once with the previously mentioned equality over a false conditional, and once using the fact that $((\text{att}_0() = \text{sk}) = \text{false}) \equiv (\text{att}_0() \neq \text{sk})$.
## 2.3. Unforgeability of hash functions: EUF-CMA

To reason over cryptographic games, a final piece of the puzzle is missing: assumptions over cryptographic primitives. For each primitive (a cipher, a signature, a hash, ...), there is a usual set of cryptographic assumptions made over it. Such assumptions are expressed as an indistinguishability between two games, and cryptographic proofs take the form of reduction-based arguments. To prove that the security of the primitive, for instance expressed as $P_R \approx P_I$, implies the security of some game $\mathcal{G}_R \approx \mathcal{G}_I$, we prove the contrapositive: assuming that there is a distinguisher against $\mathcal{G}_R \approx \mathcal{G}_I$, we build a distinguisher against $P_R \approx P_I$. In our logic, we hide those reduction-based arguments behind dedicated rules, one for each cryptographic assumption.

Consider the example of a keyed hash function $h(x, sk)$ and of the EUF-CMA assumption. Intuitively, a keyed hash function is a function that takes a message and a key, and produces a short unpredictable value. More precisely, if a key sk is secret and randomly sampled, then an attacker has a negligible probability of guessing the hash $h(m, sk)$ of any $m$, unless the attacker was directly given this value. Such a hash function is called *unforgeable*, and this is formalized in the EUF-CMA$_h$ cryptographic game:

$$ 
\begin{array}{l}
\text{EUF-CMA}_h \\
\quad 1: \quad \mathsf{sk} \stackrel{\mathcal{S}}{\leftarrow} \{0, 1\}^\eta; \\
\quad 2: \quad \mathcal{L} \leftarrow \emptyset; \\
\quad 3: \quad t, m \leftarrow \mathcal{A}^O(); \\
\quad 4: \quad \mathsf{return} (t = h(m, sk) \wedge m \notin \mathcal{L})
\end{array}
$$

$$ 
\begin{array}{l}
\text{Hashing Oracle } \mathcal{O}(x) \\
\quad 1: \quad \mathcal{L} \leftarrow \{x\} \cup \mathcal{L}; \\
\quad 2: \quad \mathsf{return} h(x, sk)
\end{array}
$$

This game asks the attacker to return a pair of values $t, m$ such that $t = h(m, sk)$. The attacker is allowed to interact with the hashing oracle $\mathcal{O}$, but it must return a $m$ that was never queried to $\mathcal{O}$. This is enforced by storing in a set $\mathcal{L}$ all oracle inputs.

We can express the security of the hash function by assuming that for all attackers $\mathcal{A}$, EUF-CMA$_h \approx$ (return false). Our goal is now to derive an inference rule which is sound under this assumption.

As a warm-up, we restrict ourselves to models where the interpretation of $h$ satisfies the EUF-CMA assumption, and analyze the validity of a few statements:

- $(h(0, sk) = \text{att}_0()) \sim \text{false is valid.}$ Otherwise, we would have a model (and thus an attacker) able to output with non-negligible probability the value of $h(0, sk)$ without having access to any other hash values. This attacker would trivially break EUF-CMA$_h$, by directly outputting $0, h(0, sk)$.

- $(h(0, sk) = \text{att}_1(sk)) \sim \text{false is not valid, because the secret key is leaked to the attacker.}$ As such, the computation of $\text{att}_1(sk)$ cannot be seen as a computation made by an adversary $\mathcal{A}^O$ in the EUF-CMA$_h$ game, and the assumption does not apply.

- $(h(0, sk) = \text{att}_1(h(1, sk))) \sim \text{false is valid.}$ Otherwise, we would have a model and thus an attacker breaking EUF-CMA$_h$: the attacker would compute $h(1, sk)$ with a call to oracle $\mathcal{O}(1)$, after which $\mathcal{L} = \{1\}$, and return $\text{att}_1(h(1, sk))$, which is the hash of $0 \notin \mathcal{L}$.

To generalize this, we need to answer the following question: under which conditions over $t$ and $m$ is $(h(m, sk) = t) \sim \text{false a valid formula?}$ We answer this by providing sufficient conditions under which the terms $t$ and $m$ can be produced by some attacker interacting with the EUF-CMA$_h$ game in such a way that $m$ is never queried to $\mathcal{O}$.

The first main condition is that all syntactic occurrences of sk in $t$ and $m$ must be as a key to $h$ (i.e. all occurrences are of the form $h(u, sk)$ for some $u$). Otherwise, the terms cannot be simulated, as the adversary $\mathcal{A}$ against EUF-CMA$_h$ does not know the key.

Once we know that sk is only used in key position, it is easy to syntactically track in $t$ and $m$ what will be computed using queries to $\mathcal{O}$: it is precisely the set of subterms
## 2.3. Unforgeability of hash functions: EUF-CMA

To reason over cryptographic games, a final piece of the puzzle is missing: assumptions over cryptographic primitives. For each primitive (a cipher, a signature, a hash, ...), there is a usual set of cryptographic assumptions made over it. Such assumptions are expressed as an indistinguishability between two games, and cryptographic proofs take the form of reduction-based arguments. To prove that the security of the primitive, for instance expressed as $P_R \approx P_I$, implies the security of some game $\mathcal{G}_R \approx \mathcal{G}_I$, we prove the contrapositive: assuming that there is a distinguisher against $\mathcal{G}_R \approx \mathcal{G}_I$, we build a distinguisher against $P_R \approx P_I$. In our logic, we hide those reduction-based arguments behind dedicated rules, one for each cryptographic assumption.

Consider the example of a keyed hash function $h(x, sk)$ and of the EUF-CMA assumption. Intuitively, a keyed hash function is a function that takes a message and a key, and produces a short unpredictable value. More precisely, if a key sk is secret and randomly sampled, then an attacker has a negligible probability of guessing the hash $h(m, sk)$ of any $m$, unless the attacker was directly given this value. Such a hash function is called *unforgeable*, and this is formalized in the EUF-CMA$_h$ cryptographic game:

$$ \begin{array}{l} \text{EUF-CMA}_h \\ \text{1: } sk \stackrel{\$}{\rightleftharpoons} \{0, 1\}^\eta; \\ \text{2: } \mathcal{L} \leftarrow \emptyset; \\ \text{3: } t, m \leftarrow \mathcal{A}^O(); \\ \text{4: } \mathbf{return} (t = h(m, sk) \wedge m \notin \mathcal{L}) \end{array} $$

$$ \begin{array}{l} \text{Hashing Oracle } \mathcal{O}(x) \\ \text{1: } \mathcal{L} \leftarrow \{x\} \cup \mathcal{L}; \\ \text{2: } \mathbf{return} h(x, sk) \end{array} $$

This game asks the attacker to return a pair of values $t, m$ such that $t = h(m, sk)$. The attacker is allowed to interact with the hashing oracle $\mathcal{O}$, but it must return a $m$ that was never queried to $\mathcal{O}$. This is enforced by storing in a set $\mathcal{L}$ all oracle inputs.

We can express the security of the hash function by assuming that for all attackers $\mathcal{A}$, EUF-CMA$_h \approx$ (return false). Our goal is now to derive an inference rule which is sound under this assumption.

As a warm-up, we restrict ourselves to models where the interpretation of $h$ satisfies the EUF-CMA assumption, and analyze the validity of a few statements:

- $(h(0, sk) = \text{att}_0()) \sim$ false is valid. Otherwise, we would have a model (and thus an attacker) able to output with non-negligible probability the value of $h(0, sk)$ without having access to any other hash values. This attacker would trivially break EUF-CMA$_h$, by directly outputting $0, h(0, sk)$.

- $(h(0, sk) = \text{att}_1(sk)) \sim$ false is not valid, because the secret key is leaked to the attacker. As such, the computation of $\text{att}_1(sk)$ cannot be seen as a computation made by an adversary $\mathcal{A}^O$ in the EUF-CMA$_h$ game, and the assumption does not apply.

- $(h(0, sk) = \text{att}_1(h(1, sk))) \sim$ false is valid. Otherwise, we would have a model and thus an attacker breaking EUF-CMA$_h$: the attacker would compute $h(1, sk)$ with a call to oracle $\mathcal{O}(1)$, after which $\mathcal{L} = \{1\}$, and return $\text{att}_1(h(1, sk))$, which is the hash of $0 \notin \mathcal{L}$.

To generalize this, we need to answer the following question: under which conditions over $t$ and $m$ is $(h(m, sk) = t) \sim$ false a valid formula? We answer this by providing sufficient conditions under which the terms $t$ and $m$ can be produced by some attacker interacting with the EUF-CMA$_h$ game in such a way that $m$ is never queried to $\mathcal{O}$.

The first main condition is that all syntactic occurrences of sk in $t$ and $m$ must be as a key to $h$ (i.e. all occurrences are of the form $h(u, sk)$ for some $u$). Otherwise, the terms cannot be simulated, as the adversary $\mathcal{A}$ against EUF-CMA$_h$ does not know the key.

Once we know that sk is only used in key position, it is easy to syntactically track in $t$ and $m$ what will be computed using queries to $\mathcal{O}$: it is precisely the set of subterms
<figure><img src="image_5.png" /><figcaption>Fig. 3. Authentication game for the BASIC HASH protocol.</figcaption></figure>

of the form $h(x, sk)$, i.e. $S_{sk}^h(t, m) = \{h(u, sk) | h(u, sk) \text{ subterm of } t \text{ or } m\}$. Using this set, we can then define a formula, inside our logic, expressing that all previously seen hash values are distinct from $m$. Those two conditions are sufficient to obtain a rule enabling us to use EUF-CMA to establish indistinguishabilities in the logic:

$$ \text{EUF-CMA} \quad \frac{\bigwedge_{h(u,sk) \in S_{sk}^h(t,m)} ((u=m) \sim \text{false})}{(h(m,sk)=t) \sim \text{false}} \quad \text{sk only occurs as } h(x,sk) \text{ in } t \text{ and } m $$

This rule has a logical premise, which becomes a proof obligation when the rule is applied to a proof goal, and a syntactic side condition automatically checked by Squirrel.

### 3. MODELING INTERACTIVE PROTOCOLS WITH RECURSIVE FUNCTIONS

Now that we have introduced the core CCSA framework, let us turn to how cryptographic protocols are modeled. Compared to the simple games of the previous section, protocols are concurrent systems, involving several communicating agents. An agent may for instance be a key server, a bank, a user's terminal... When analyzing the security of a protocol, it is desirable to make worst-case assumptions. A typical one is that the adversary has full control over the network: it receives all messages output by protocol agents, and is tasked with feeding inputs to them, with messages resulting from arbitrary computations. We also assume that the adversary schedules the actions of the protocol's agents: it decides when to spawn a new session, when to advance in a session, ... This can actually be modeled using cryptographic games, representing the agents as oracles to which the adversary has access. Adversarial computations then induce a sequence of interactions with the protocol's agents, i.e. an execution trace of the protocol. Following this style, quantifying over all adversaries implies quantifying over all execution traces. We present this approach in more details in what follows, illustrating it on a simplified version of the BASIC HASH protocol [Brusò et al. 2010].

#### 3.1. An example: BASIC HASH protocol

The BASIC HASH protocol is a simple RFID protocol in which a tag $\mathcal{T}$ tries to authenticate itself to a reader $\mathcal{R}$. This is an access control protocol: e.g. the tag may be embedded in an RFID fob, and the reader could guard access to some building. The tag and the reader both share a secret key sk. Whenever the tag wants to authenticate itself to the reader, it samples a random value $n$, hashes it with sk using an unforgeable keyed hash function as presented in Section 2.3, and sends the pair $\langle n, h(n, sk) \rangle$ of the name and its hash digest to the reader. The reader can check that a message $x$ it received from the network was generated by the tag by extracting the first component $fst(x)$ of $x$, re-computing its hash using the secret key sk and checking that this yields the second component $snd(x)$ of its input.

*Authentication game.* We can express the fact that this protocol provides some form of authentication using the cryptographic game presented in Figure 3. The definitions of $\mathcal{T}$ and $\mathcal{R}_r$ correspond to the tag and reader agents described above, with a single addition that will be useful to express the security property: before sending its output
<figure><img src="image_5.png" /><figcaption>Fig. 3. Authentication game for the BASIC HASH protocol.</figcaption></figure>

of the form $h(x, sk)$, i.e. $S_{sk}^h(t, m) = \{h(u, sk) | h(u, sk) \text{ subterm of } t \text{ or } m\}$. Using this set, we can then define a formula, inside our logic, expressing that all previously seen hash values are distinct from $m$. Those two conditions are sufficient to obtain a rule enabling us to use EUF-CMA to establish indistinguishabilities in the logic:

$$ \text{EUF-CMA} \quad \frac{\bigwedge_{h(u,sk) \in S_{sk}^h(t,m)} ((u=m) \sim \text{false})}{(h(m,sk)=t) \sim \text{false}} \quad \text{sk only occurs as } h(x,sk) \text{ in } t \text{ and } m $$

This rule has a logical premise, which becomes a proof obligation when the rule is applied to a proof goal, and a syntactic side condition automatically checked by Squirrel.

### 3. MODELING INTERACTIVE PROTOCOLS WITH RECURSIVE FUNCTIONS

Now that we have introduced the core CCSA framework, let us turn to how cryptographic protocols are modeled. Compared to the simple games of the previous section, protocols are concurrent systems, involving several communicating agents. An agent may for instance be a key server, a bank, a user's terminal... When analyzing the security of a protocol, it is desirable to make worst-case assumptions. A typical one is that the adversary has full control over the network: it receives all messages output by protocol agents, and is tasked with feeding inputs to them, with messages resulting from arbitrary computations. We also assume that the adversary schedules the actions of the protocol's agents: it decides when to spawn a new session, when to advance in a session, ... This can actually be modeled using cryptographic games, representing the agents as oracles to which the adversary has access. Adversarial computations then induce a sequence of interactions with the protocol's agents, i.e. an execution trace of the protocol. Following this style, quantifying over all adversaries implies quantifying over all execution traces. We present this approach in more details in what follows, illustrating it on a simplified version of the BASIC HASH protocol [Brusò et al. 2010].

#### 3.1. An example: BASIC HASH protocol

The BASIC HASH protocol is a simple RFID protocol in which a tag $\mathcal{T}$ tries to authenticate itself to a reader $\mathcal{R}$. This is an access control protocol: e.g. the tag may be embedded in an RFID fob, and the reader could guard access to some building. The tag and the reader both share a secret key sk. Whenever the tag wants to authenticate itself to the reader, it samples a random value $n$, hashes it with sk using an unforgeable keyed hash function as presented in Section 2.3, and sends the pair $\langle n, h(n, sk) \rangle$ of the name and its hash digest to the reader. The reader can check that a message $x$ it received from the network was generated by the tag by extracting the first component $fst(x)$ of $x$, re-computing its hash using the secret key sk and checking that this yields the second component $snd(x)$ of its input.

*Authentication game.* We can express the fact that this protocol provides some form of authentication using the cryptographic game presented in Figure 3. The definitions of $\mathcal{T}$ and $\mathcal{R}_r$ correspond to the tag and reader agents described above, with a single addition that will be useful to express the security property: before sending its output
$x = \langle n, h(n, sk) \rangle$ to the reader, the tag logs $x$ into a set $\mathcal{L}$. Further, $\mathcal{R}_i$ corresponds to an idealized reader, which checks that its input $x$ originates from $\mathcal{T}$ by directly verifying that $x$ appears in the log $\mathcal{L}$. Intuitively, the idealized reader looks, across space and time, into the past internal memories of the tag to check whether it indeed generated $x$. Obviously, $\mathcal{R}_i$ is only useful as a trick to model the expected authentication property, and cannot be physically implemented.

The cryptographic game $\mathcal{G}(\mathcal{R})$, parameterized by the reader $\mathcal{R} \in \{\mathcal{R}_r, \mathcal{R}_i\}$, samples the secret key sk, initializes the log $\mathcal{L}$, and runs the adversary $\mathcal{A}^{\mathcal{T},\mathcal{R}}$ by letting it interact with the tag and reader oracles. The adversary must try to guess a bit $b$ indicating whether it is interacting with the real or ideal reader $\mathcal{R}$: its guess $b$ is the final result of the game. The protocol is secure if $\mathcal{A}$ has a negligible advantage in guessing the correct bit $b$, i.e. if the computational indistinguishability $\mathcal{G}(\mathcal{R}_r) \approx \mathcal{G}(\mathcal{R}_i)$ holds. Indeed, if an attacker can make $\mathcal{R}_r$ accept while breaking authentication (i.e. no corresponding tag produced the message), trying to do the same execution with $\mathcal{R}_i$ would fail by construction, making it trivial to distinguish the two worlds.

## 3.2. Modeling protocol executions

During its execution, $\mathcal{A}$ can call the tag and reader oracles any number of times and according to any interleaving. We are going to model the interaction of $\mathcal{A}$ with the protocol agents $\mathcal{T}, \mathcal{R}$ along an execution trace $\text{tr}$ representing a fixed but arbitrary interleaving. Thus, an execution trace $\text{tr}$ is a finite sequence $\tau_1, \dots, \tau_n$ of timestamps, where the $j$-th timestamp $\tau_j$ in the trace represents the agent the adversary interacted with at this step. To distinguish multiple interactions with the same agents, actions are indexed by a unique replication index $i$ in some set of indices $\mathcal{I}$. For BASIC HASH, we use $\tau = \text{T}(i)$ and $\tau = \text{R}(i)$ for an interaction with respectively the tag and the reader. For convenience, we also force $\tau_1$ to a special value $\text{init}$.

$$ \mathcal{T} ::= \tau_1, \dots, \tau_n \qquad \tau_i ::= \text{init} \mid \text{T}(i) \mid \text{R}(i) \qquad (n \in \mathbb{N}, i \in \mathcal{I}) $$

**Modeling execution traces.** We assume a typed logic, to enable reasoning over different kinds of objects. Models of the logic provide an interpretation domain for each type, where for instance `message` is interpreted as the set of bitstrings and `bool` as $\{0, 1\}$. Intuitively, the type of all terms used in Section 2 is `message` or `bool`, with e.g. the equality function symbol `=` typed as `message` → `message` → `bool`. The types `index` and `timestamp` respectively represent the sets of indices $\mathcal{I}$ and timestamps $\mathcal{T}$, and we use function symbols `T` and `R`, both of type `index` → `timestamp`, to build timestamps from indices, and `init`: `timestamp` for the initial timestamp. The execution trace $\text{tr}$ is implicitly encoded using two function symbols:

$$ \text{happens} : \text{timestamp} \to \text{bool} \qquad \cdot < \cdot : \text{timestamp} \to \text{timestamp} \to \text{bool} $$

where `happens(\tau)` states that $\tau$ has been scheduled in the execution trace, and $\tau < \tau'$ that $\tau$ occurred before $\tau'$ in the trace. Each model $\mathcal{M}$ of the logic fixes the execution trace by interpreting the types and function symbols above. We require, through an ad hoc restriction on models of the logic, that the interpretation of `index` in any model is finite and independent of the security parameter $\eta$. Further, we assume that any scheduled timestamp uniquely corresponds to either `init`, some $\text{T}(i)$ or some $\text{R}(i)$.

**Modeling the game's execution.** In the logic, the interaction of the adversary $\mathcal{A}$ with the oracles $\mathcal{T}$ and $\mathcal{R}$ along an execution trace is modeled using several mutually recursive functions called macros. A macro is identified by its name `m` and is evaluated at a particular timestamp $\tau$: informally, `m@\tau` refers to the value of `m` at point $\tau$ in the execution. We will use the following macros: `input@\tau` and `output@\tau` denote the messages input and output by the oracle scheduled at time $\tau$ in the execution trace;
$x = \langle n, h(n, sk) \rangle$ to the reader, the tag logs $x$ into a set $\mathcal{L}$. Further, $\mathcal{R}_i$ corresponds to an idealized reader, which checks that its input $x$ originates from $\mathcal{T}$ by directly verifying that $x$ appears in the log $\mathcal{L}$. Intuitively, the idealized reader looks, across space and time, into the past internal memories of the tag to check whether it indeed generated $x$. Obviously, $\mathcal{R}_i$ is only useful as a trick to model the expected authentication property, and cannot be physically implemented.

The cryptographic game $\mathcal{G}(\mathcal{R})$, parameterized by the reader $\mathcal{R} \in \{\mathcal{R}_r, \mathcal{R}_i\}$, samples the secret key sk, initializes the log $\mathcal{L}$, and runs the adversary $\mathcal{A}^{\mathcal{T},\mathcal{R}}$ by letting it interact with the tag and reader oracles. The adversary must try to guess a bit $b$ indicating whether it is interacting with the real or ideal reader $\mathcal{R}$: its guess $b$ is the final result of the game. The protocol is secure if $\mathcal{A}$ has a negligible advantage in guessing the correct bit $b$, i.e. if the computational indistinguishability $\mathcal{G}(\mathcal{R}_r) \approx \mathcal{G}(\mathcal{R}_i)$ holds. Indeed, if an attacker can make $\mathcal{R}_r$ accept while breaking authentication (i.e. no corresponding tag produced the message), trying to do the same execution with $\mathcal{R}_i$ would fail by construction, making it trivial to distinguish the two worlds.

## 3.2. Modeling protocol executions

During its execution, $\mathcal{A}$ can call the tag and reader oracles any number of times and according to any interleaving. We are going to model the interaction of $\mathcal{A}$ with the protocol agents $\mathcal{T}, \mathcal{R}$ along an execution trace $\text{tr}$ representing a fixed but arbitrary interleaving. Thus, an execution trace $\text{tr}$ is a finite sequence $\tau_1, \dots, \tau_n$ of timestamps, where the $j$-th timestamp $\tau_j$ in the trace represents the agent the adversary interacted with at this step. To distinguish multiple interactions with the same agents, actions are indexed by a unique replication index $i$ in some set of indices $\mathcal{I}$. For BASIC HASH, we use $\tau = \text{T}(i)$ and $\tau = \text{R}(i)$ for an interaction with respectively the tag and the reader. For convenience, we also force $\tau_1$ to a special value $\text{init}$.

$$ \mathcal{T} ::= \tau_1, \dots, \tau_n \qquad \tau_i ::= \text{init} \mid \text{T}(i) \mid \text{R}(i) \qquad (n \in \mathbb{N}, i \in \mathcal{I}) $$

**Modeling execution traces.** We assume a typed logic, to enable reasoning over different kinds of objects. Models of the logic provide an interpretation domain for each type, where for instance `message` is interpreted as the set of bitstrings and `bool` as $\{0, 1\}$. Intuitively, the type of all terms used in Section 2 is `message` or `bool`, with e.g. the equality function symbol `=` typed as `message` → `message` → `bool`. The types `index` and `timestamp` respectively represent the sets of indices $\mathcal{I}$ and timestamps $\mathcal{T}$, and we use function symbols `T` and `R`, both of type `index` → `timestamp`, to build timestamps from indices, and `init`: `timestamp` for the initial timestamp. The execution trace $\text{tr}$ is implicitly encoded using two function symbols:

$$ \text{happens} : \text{timestamp} \to \text{bool} \qquad \cdot < \cdot : \text{timestamp} \to \text{timestamp} \to \text{bool} $$

where `happens(\tau)` states that $\tau$ has been scheduled in the execution trace, and $\tau < \tau'$ that $\tau$ occurred before $\tau'$ in the trace. Each model $\mathcal{M}$ of the logic fixes the execution trace by interpreting the types and function symbols above. We require, through an ad hoc restriction on models of the logic, that the interpretation of `index` in any model is finite and independent of the security parameter $\eta$. Further, we assume that any scheduled timestamp uniquely corresponds to either `init`, some $\text{T}(i)$ or some $\text{R}(i)$.

**Modeling the game's execution.** In the logic, the interaction of the adversary $\mathcal{A}$ with the oracles $\mathcal{T}$ and $\mathcal{R}$ along an execution trace is modeled using several mutually recursive functions called macros. A macro is identified by its name `m` and is evaluated at a particular timestamp $\tau$: informally, `m@\tau` refers to the value of `m` at point $\tau$ in the execution. We will use the following macros: `input@\tau` and `output@\tau` denote the messages input and output by the oracle scheduled at time $\tau$ in the execution trace;
and frame@τ is roughly the sequence of all messages output by any agent during the execution up to timestamp τ. The frame is crucial to express security properties, as it represents the full list of messages seen by the attacker. We assume a function symbol pred : timestamp → timestamp that maps any scheduled timestamp different from init to its predecessor in the execution trace, and all other timestamps to a fixed constant undef, distinct from all scheduled timestamps. The macros can be defined as follows for the game G(ℝᵣ) using the real reader:

$$
\begin{align*}
\text{input}_r @ \tau &= \text{match } \tau \text{ with} &
\begin{array}{@{}l@{}}
  \text{frame}_r @ \tau = \text{match } \tau \text{ with} \\
  \quad | \text{init} \to \text{empty} \\
  \quad | \text{att}_{\tau}(\text{frame}_r @ \text{pred}(\tau)) \\
  \quad | \text{init} \to \emptyset
\end{array} \\
\text{output}_r @ \tau &= \text{match } \tau \text{ with} &
\begin{array}{@{}l@{}}
  \text{snd}(\text{input}_r @ \tau) \\
  \quad | \text{init} \to \emptyset \\
  \quad | \text{att}_{\tau}(\text{input}_r @ \tau) \\
  \quad | \text{init} \to \emptyset \\
  \quad | \text{att}_{\tau}(\text{frame}_r @ \tau) \\
  \quad | \text{init} \to \emptyset \\
  \quad | \text{att}_{\tau}(\text{frame}_r @ \text{pred}(\tau)) \\
  \quad | \text{init} \to \emptyset \\
  \quad | \text{att}_{\tau}(\text{frame}_r @ \text{pred}(\tau)) \\
  \quad | \text{init} \to \emptyset
\end{array}
\end{align*}
$$

where empty is a symbol of type **message** representing the empty bitstring, and where we generalized names to be of type **index** → **message**, so that each $n(i)$ is an independent fresh name. The *r* subscript indicates that these macros are for the game using the real reader. The macros definitions for the game with the ideal reader $G(ℝ_i)$, subscripted by *i*, are identical except for the output macro: we only need to introduce a macro $\mathcal{L}@\tau$ for the value of the log $\mathcal{L}$ after the execution of the oracle at $\tau$, and to modify the $R(i)$ case of output:

$$
\begin{align*}
\text{output}_i @ \tau &= \text{match } \tau \text{ with} &
  \begin{array}{@{}l@{}}
    \mathcal{L} @ \tau = \text{match } \tau \text{ with} \\
    \quad | R(i) \to \text{input}_i @ \tau \in \mathcal{L} @ \tau \\
    \quad | \dots \to \dots \text{ (as before)}
  \end{array} \\
\text{output}_i @ \tau &= \text{match } \tau \text{ with} &
  \begin{array}{@{}l@{}}
    \text{snd}(\text{input}_i @ \tau) \\
    \quad | \text{init} \to \emptyset \\
    \quad | \text{att}_{\tau}(\text{output}_i @ \tau) \cup \mathcal{L} @ \text{pred}(\tau) \\
    \quad | \text{init} \to \emptyset \\
    \quad | \text{att}_{\tau}(\text{frame}_i @ \tau) \\
    \quad | \text{init} \to \emptyset
  \end{array}
\end{align*}
$$

Then, the formula frame_r @ τ ~ frame_i @ τ expresses the fact that, for any model M defining an execution trace tr and an adversary A, the adversary has a negligible probability of distinguishing the real and ideal versions of the protocol, i.e. G(ℝᵣ) ≈ G(ℝᵢ) holds along this particular execution trace (see Section 3.3 below for a discussion of the security guarantees provided by this formula).

*Cryptographic reasoning with recursive functions.* The EUF-CMA reasoning rule presented in Section 2.3 does not directly apply to terms containing recursive definitions: we need to be able to reason over the occurrences of the hash function inside terms, and thus possibly inside an arbitrary recursive unfolding. A first way to fix the EUF-CMA rule is to forbid any occurrence of a hash in all the recursive functions occurring inside a term, but it is of course too limiting: in BASIC HASH, we have for instance a set of hash occurrences of the form $h(n(i), sk)$ in output_r. We need to be able to reason over such a set, for instance using some universal quantification over indices or timestamps. We formally introduce such constructions in Section 4.2, and extend the cryptographic rules in Section 4.4.

*Implementation in Squirrel.* The encoding of protocols using macros as described above can be generalized to support a large class of security protocols. Given a protocol P, we can use the same definitions for frame and input, and we only need to adapt the definition of output according to the protocol specification, and, if necessary, introduce additional macros for the protocol's mutable variables (such as the macro L for the log L). This method is expressive enough to encode complex protocol behaviors, and allows all relevant information to be expressed as messages that our logic can handle.
and frame@τ is roughly the sequence of all messages output by any agent during the execution up to timestamp τ. The frame is crucial to express security properties, as it represents the full list of messages seen by the attacker. We assume a function symbol pred : timestamp → timestamp that maps any scheduled timestamp different from init to its predecessor in the execution trace, and all other timestamps to a fixed constant undef, distinct from all scheduled timestamps. The macros can be defined as follows for the game G(ℝᵣ) using the real reader:

$$
\begin{align*}
\text{input}_r @ \tau &= \text{match } \tau \text{ with} &
\begin{array}{@{}l@{}}
\text{frame}_r @ \tau = \text{match } \tau \text{ with} \\
\quad | \text{init} \to \text{empty} \\
\quad | \text{att}_{\tau}(\text{frame}_r @ \text{pred}(\tau))
\end{array} \\
& & \text{output}_r @ \tau = \text{match } \tau \text{ with} \\
& & \quad | \text{init} \to \text{empty} \\
& & \quad | \text{T}(i) \to \langle \text{n}(i), \text{h}(\text{n}(i), \text{sk}) \rangle \\
& & \quad | \text{R}(i) \to \text{h}(\text{fst}(\text{input}_r @ \tau), \text{sk}) = \text{snd}(\text{input}_r @ \tau)
\end{align*}
$$

where empty is a symbol of type **message** representing the empty bitstring, and where we generalized names to be of type **index** → **message**, so that each n(i) is an independent fresh name. The r subscript indicates that these macros are for the game using the real reader. The macros definitions for the game with the ideal reader G(ℝᵢ), subscripted by i, are identical except for the output macro: we only need to introduce a macro L@τ for the value of the log L after the execution of the oracle at τ, and to modify the R(i) case of output:

$$
\begin{align*}
\text{output}_i @ \tau &= \text{match } \tau \text{ with} &
\begin{array}{@{}l@{}}
\mathcal{L} @ \tau = \text{match } \tau \text{ with} \\
\quad | \text{R}(i) \to \text{input}_i @ \tau \in \mathcal{L} @ \tau \\
\quad | \dots \to \dots \text{ (as before)}
\end{array} \\
& & \text{init} \to \emptyset \\
& & \text{T}(i) \to \{\text{output}_i @ \tau\} \cup \mathcal{L} @ \text{pred}(\tau) \\
& & \text{R}(i) \to \mathcal{L} @ \text{pred}(\tau)
\end{align*}
$$

Then, the formula frame<sub>r</sub>@τ ~ frame<sub>i</sub>@τ expresses the fact that, for any model M
defining an execution trace tr and an adversary A, the adversary has a negligible
probability of distinguishing the real and ideal versions of the protocol, i.e. G(ℝ<sub>r</sub>) ~
G(ℝ<sub>i</sub>) holds along this particular execution trace (see Section 3.3 below for a discussion
of the security guarantees provided by this formula).

Cryptographic reasoning with recursive functions. The EUF-CMA reasoning rule presented in Section 2.3 does not directly apply to terms containing recursive definitions: we need to be able to reason over the occurrences of the hash function inside terms, and thus possibly inside an arbitrary recursive unfolding. A first way to fix the EUF-CMA rule is to forbid any occurrence of a hash in all the recursive functions occurring inside a term, but it is of course too limiting: in BASIC HASH, we have for instance a set of hash occurrences of the form h(n(i), sk) in output<sub>r</sub>. We need to be able to reason over such a set, for instance using some universal quantification over indices or timestamps. We formally introduce such constructions in Section 4.2, and extend the cryptographic rules in Section 4.4.

*Implementation in Squirrel.* The encoding of protocols using macros as described above can be generalized to support a large class of security protocols. Given a protocol *P*, we can use the same definitions for *frame* and *input*, and we only need to adapt the definition of *output* according to the protocol specification, and, if necessary, introduce additional macros for the protocol’s mutable variables (such as the macro *L* for the log *L*). This method is expressive enough to encode complex protocol behaviors, and allows all relevant information to be expressed as messages that our logic can handle.
However, it is arguably not very intuitive to manipulate for users. To help with that, Squirrel allows users to describe protocols as processes in a process algebra (a variant of the applied π-calculus), and automatically translates them as macros (the actual definition of Squirrel macros is slightly more involved than the one presented here, we refer readers to [Baelde et al. 2022] for details).

### 3.3. The issue of asymptotic security

With the modeling style described here for protocols, we always reason on an arbitrary but fixed trace. When proving a property, we show that it holds (up to negligible probability) in all models of the logic, and the model includes the interpretation of the order on timestamps, i.e. the interleaving of actions, as well as the interpretation of all attacker function symbols. In particular, this means that in any given model, the trace and the interpretation of adversarial functions is fixed, and only then do the security parameter η and random tape ρ vary. In other words, when proving a property φ, what we establish can informally be described by the formula:

$$ \forall \text{trace tr. } \forall \text{adversary } \mathcal{A}. \text{Pr}_\rho(\phi \text{ holds in tr against } \mathcal{A}) \text{ is overwhelming in } \eta. $$

While such a statement gives good security guarantees, it is weaker than what is commonly expected. In cryptographic games, the adversary is indeed given access to the protocol through oracles it may call at will any (polynomial) number of times. That is, the adversary can choose the trace, rather than having it imposed on him. In particular, the length of the trace may be chosen by the adversary and thus depend on η, while it is fixed in our model. That would correspond to the stronger (informal) formula:

$$ \forall \text{adversary } \mathcal{A}. \text{Pr}_\rho(\phi \text{ holds in tr chosen by } \mathcal{A}) \text{ is overwhelming in } \eta. $$

It is possible to overcome this limitation by changing the way we model protocols, to let the adversary adaptively choose the trace during the protocol execution. However, such alternatives have not yet been explored in practice.

## 4. THE GENERAL LOGIC & PROOF SYSTEM

We have considered so far a typed language with first-order terms and a single indistinguishability predicate, with inference rules that can be expressed as axioms in first-order logic. Except for the addition of recursively defined functions, all this fits within the original CCSA logic of [Bana and Comon-Lundh 2014], which is plain first-order logic. Thus, proving statements in that logic can be done using any proof system for classical first-order logic; only the CCSA axiom schemes would reflect the intended probabilistic semantics of terms and the cryptographic assumptions on primitives.

We have seen, however, that syntactic side conditions, which are needed for cryptographic rules, cannot be easily lifted to terms containing recursive definitions. In addition, the logic appears ill-suited for some security properties. Recall the BASIC HASH example, whose security we defined by using a real and an ideal system. Yet, the intuitive security property should only be about a high-level fact verified by all executions of the real system: whenever a reader accepts, the value it received was produced by an honest tag.

To improve this aspect of the logic, a core idea is to introduce a more specific logic, where special status is given to terms of type *bool*. We have seen axioms involving indistinguishability, of the form $t \sim \text{true}$ or $t \sim \text{false}$. For such formulas, using computational indistinguishability for all PPTM distinguishers is overkill, and we can take a much simpler approach: $t \sim \text{true}$ simply means that $t$ is true with overwhelming probability. Further, it is convenient to view $t$ itself as a specific kind of formula: to this effect, we can use function symbols representing propositional connectives, as we did for the if-then-else construction; less obviously, the same can be done for quantifiers. In that
However, it is arguably not very intuitive to manipulate for users. To help with that, Squirrel allows users to describe protocols as processes in a process algebra (a variant of the applied π-calculus), and automatically translates them as macros (the actual definition of Squirrel macros is slightly more involved than the one presented here, we refer readers to [Baelde et al. 2022] for details).

### 3.3. The issue of asymptotic security

With the modeling style described here for protocols, we always reason on an arbitrary but fixed trace. When proving a property, we show that it holds (up to negligible probability) in all models of the logic, and the model includes the interpretation of the order on timestamps, i.e. the interleaving of actions, as well as the interpretation of all attacker function symbols. In particular, this means that in any given model, the trace and the interpretation of adversarial functions is fixed, and only then do the security parameter η and random tape ρ vary. In other words, when proving a property φ, what we establish can informally be described by the formula:

$$ \forall \text{trace tr. } \forall \text{adversary } \mathcal{A}. \text{Pr}_\rho(\phi \text{ holds in tr against } \mathcal{A}) \text{ is overwhelming in } \eta. $$

While such a statement gives good security guarantees, it is weaker than what is commonly expected. In cryptographic games, the adversary is indeed given access to the protocol through oracles it may call at will any (polynomial) number of times. That is, the adversary can choose the trace, rather than having it imposed on him. In particular, the length of the trace may be chosen by the adversary and thus depend on η, while it is fixed in our model. That would correspond to the stronger (informal) formula:

$$ \forall \text{adversary } \mathcal{A}. \text{Pr}_\rho(\phi \text{ holds in tr chosen by } \mathcal{A}) \text{ is overwhelming in } \eta. $$

It is possible to overcome this limitation by changing the way we model protocols, to let the adversary adaptively choose the trace during the protocol execution. However, such alternatives have not yet been explored in practice.

## 4. THE GENERAL LOGIC & PROOF SYSTEM

We have considered so far a typed language with first-order terms and a single indistinguishability predicate, with inference rules that can be expressed as axioms in first-order logic. Except for the addition of recursively defined functions, all this fits within the original CCSA logic of [Bana and Comon-Lundh 2014], which is plain first-order logic. Thus, proving statements in that logic can be done using any proof system for classical first-order logic; only the CCSA axiom schemes would reflect the intended probabilistic semantics of terms and the cryptographic assumptions on primitives.

We have seen, however, that syntactic side conditions, which are needed for cryptographic rules, cannot be easily lifted to terms containing recursive definitions. In addition, the logic appears ill-suited for some security properties. Recall the BASIC HASH example, whose security we defined by using a real and an ideal system. Yet, the intuitive security property should only be about a high-level fact verified by all executions of the real system: whenever a reader accepts, the value it received was produced by an honest tag.

To improve this aspect of the logic, a core idea is to introduce a more specific logic, where special status is given to terms of type *bool*. We have seen axioms involving indistinguishability, of the form $t \sim \text{true}$ or $t \sim \text{false}$. For such formulas, using computational indistinguishability for all PPTM distinguishers is overkill, and we can take a much simpler approach: $t \sim \text{true}$ simply means that $t$ is true with overwhelming probability. Further, it is convenient to view $t$ itself as a specific kind of formula: to this effect, we can use function symbols representing propositional connectives, as we did for the if-then-else construction; less obviously, the same can be done for quantifiers. In that
context, $t$ will be called a *local formula*, while the real first-order formulas are called *global*. It turns out that CCSA proofs tend to intensively reason on local formulas. This calls for a proof system that conveniently handles these like proper formulas. Squirrel comes with one such proof system, which we present in this section.

## 4.1. Higher-order terms with a relaxed semantics

Before properly introducing local and global formulas and their proof systems, we must come back to the semantics of terms. Indeed, since [Baelde et al. 2023], the logic behind Squirrel features higher-order terms. There have been several motivations for this significant generalization of the original CCSA logic. First, Squirrel developments predominantly consist of proofs of local formulas, and higher-order features at this level help structure these proofs in a modular way, and re-use them. Second, the constraints of the original CCSA logic, namely that all terms are interpreted as PPTMs, make sense for modeling cryptographic protocols and adversaries but are sometimes too restrictive when writing proofs. For instance, it can be useful to talk about the discrete logarithm over finite groups, even though this operation is (hopefully) not PTIME. It can also be useful to quantify over infinite types in local formulas, e.g. to specify properties of primitives over messages: anticipating on what follows, we will be able to write local formulas such as $\forall x, y : \text{message}$. $\text{fst}(\langle x, y \rangle) = x$.

The terms of our logic are thus simply-typed $\lambda$-calculus terms, additionally featuring recursive definitions. In the tool, some limited forms of polymorphism are even available, but we leave them unaccounted for in the theory. Each type $\tau$ is interpreted in a model $\mathbb{M}$ as a family of sets $[[\tau]]_{\mathbb{M}}^{\eta}$ indexed by the security parameter $\eta$, with $[[\tau_1 \to \tau_2]]_{\mathbb{M}}^{\eta} = [[\tau_1]]_{\mathbb{M}}^{\eta} \to [[\tau_2]]_{\mathbb{M}}^{\eta}$. We require that $[[\text{bool}]]_{\mathbb{M}}^{\eta} = \{0, 1\}$ and $[[\text{message}]]_{\mathbb{M}}^{\eta} = \{0, 1\}^*$ for all $\mathbb{M}$ and $\eta$. The potential dependency in $\eta$ is however crucial e.g. to faithfully model the finite groups used in Diffie-Hellman key exchanges.

Terms are no longer interpreted as PPTMs, but more generally as discrete random variables, i.e. functions from random tapes to the desired domain. More precisely, a model fixes a set of finite tapes $T_{\mathbb{M},\eta}$ for each $\eta$, and we let $RV_{\mathbb{M}}(\tau)$ be the set of all $\eta$-indexed sequences of functions from $T_{\mathbb{M},\eta}$ to $[[\tau]]_{\mathbb{M}}^{\eta}$. Then, given $\mathbb{M}$, $\eta$ and $\rho$, any term $t$ of type $\tau$ is interpreted as $(\rho \in T_{\mathbb{M},\eta} \mapsto [[t]]_{\mathbb{M}}^{\eta,\rho})_{\eta \in \mathbb{N}} \in RV_{\mathbb{M}}(\tau)$ as follows:

$$ 
\begin{align*}
[[x]]_{\mathbb{M}}^{\eta, \rho} &= \mathbb{M}(x)(\eta, \rho) \\
[[t \ t']_{\mathbb{M}}^{\eta, \rho} &= [[t]]_{\mathbb{M}}^{\eta, \rho} ([[t']_{\mathbb{M}}^{\eta, \rho}) \\
[[\lambda(x : \tau').t]]_{\mathbb{M}}^{\eta, \rho} &= (a \in [[\tau']_{\mathbb{M}}^{\eta} \mapsto [[t]]_{\mathbb{M}[x/a]}^{\eta, \rho}])
\end{align*}
$$

where $\mathbb{M}(x)$ is the interpretation of $x$ in $\mathbb{M}$, and $\mathbb{M}[x/a]$ is the model modified to interpret $x$ as a random variable $X$ such that $X(\eta, \rho) = a$. Note that the interpretation of a term only depends on the interpretation of its subterms for the same values of $\eta$ and $\rho$, and thus the value of $\mathbb{M}[x/a](x)$ is only relevant on $\eta, \rho$. We refer the reader to [Baelde et al. 2023] for the full details, including the interpretation of recursive definitions when they satisfy a suitable well-foundedness condition, as well as how to check that some terms do correspond to PPTM computations in order to apply cryptographic assumptions.

While it could seem more natural to have infinite tapes, rather than finite but arbitrarily long ones, this has technical motivations. It ensures that all functions computed on tapes actually correspond to random variables, i.e. that they are measurable. This restriction of our logic (and of the original CCSA logic) is not limiting when it comes to modeling cryptographic protocols and attackers, which all run in PTIME. It is however crucial that the length of tapes can grow with $\eta$. The restriction to finite tapes is standard in formal cryptographic reasoning: it is present, e.g., in approaches based on Hoare logics [Barthe et al. 2011; Petcher and Morrisett 2015; Basin et al. 2020].
context, $t$ will be called a *local formula*, while the real first-order formulas are called *global*. It turns out that CCSA proofs tend to intensively reason on local formulas. This calls for a proof system that conveniently handles these like proper formulas. Squirrel comes with one such proof system, which we present in this section.

## 4.1. Higher-order terms with a relaxed semantics

Before properly introducing local and global formulas and their proof systems, we must come back to the semantics of terms. Indeed, since [Baelde et al. 2023], the logic behind Squirrel features higher-order terms. There have been several motivations for this significant generalization of the original CCSA logic. First, Squirrel developments predominantly consist of proofs of local formulas, and higher-order features at this level help structure these proofs in a modular way, and re-use them. Second, the constraints of the original CCSA logic, namely that all terms are interpreted as PPTMs, make sense for modeling cryptographic protocols and adversaries but are sometimes too restrictive when writing proofs. For instance, it can be useful to talk about the discrete logarithm over finite groups, even though this operation is (hopefully) not PTIME. It can also be useful to quantify over infinite types in local formulas, e.g. to specify properties of primitives over messages: anticipating on what follows, we will be able to write local formulas such as $\forall x, y : \text{message}$. $\text{fst}(\langle x, y \rangle) = x$.

The terms of our logic are thus simply-typed $\lambda$-calculus terms, additionally featuring recursive definitions. In the tool, some limited forms of polymorphism are even available, but we leave them unaccounted for in the theory. Each type $\tau$ is interpreted in a model $\mathbb{M}$ as a family of sets $[[\tau]]_{\mathbb{M}}^{\eta}$ indexed by the security parameter $\eta$, with $[[\tau_1 \to \tau_2]]_{\mathbb{M}}^{\eta} = [[\tau_1]]_{\mathbb{M}}^{\eta} \to [[\tau_2]]_{\mathbb{M}}^{\eta}$. We require that $[[\text{bool}]]_{\mathbb{M}}^{\eta} = \{0, 1\}$ and $[[\text{message}]]_{\mathbb{M}}^{\eta} = \{0, 1\}^*$ for all $\mathbb{M}$ and $\eta$. The potential dependency in $\eta$ is however crucial e.g. to faithfully model the finite groups used in Diffie-Hellman key exchanges.

Terms are no longer interpreted as PPTMs, but more generally as discrete random variables, i.e. functions from random tapes to the desired domain. More precisely, a model fixes a set of finite tapes $T_{\mathbb{M},\eta}$ for each $\eta$, and we let $RV_{\mathbb{M}}(\tau)$ be the set of all $\eta$-indexed sequences of functions from $T_{\mathbb{M},\eta}$ to $[[\tau]]_{\mathbb{M}}^{\eta}$. Then, given $\mathbb{M}$, $\eta$ and $\rho$, any term $t$ of type $\tau$ is interpreted as $(\rho \in T_{\mathbb{M},\eta} \mapsto [[t]]_{\mathbb{M}}^{\eta,\rho})_{\eta \in \mathbb{N}} \in RV_{\mathbb{M}}(\tau)$ as follows:

$$ 
\begin{align*}
[[x]]_{\mathbb{M}}^{\eta,\rho} &= \mathbb{M}(x)(\eta, \rho) \\
[[t \ t']_{\mathbb{M}}^{\eta,\rho} &= [[t]]_{\mathbb{M}}^{\eta,\rho}([[[t]]_{\mathbb{M}}^{\eta,\rho}) \\
[[\lambda(x : \tau').t]]_{\mathbb{M}}^{\eta,\rho} &= (a \in [[\tau']_{\mathbb{M}}^{\eta} \mapsto [[t]]_{\mathbb{M}[x/a]}^{\eta,\rho}])
\end{align*}
$$

where $\mathbb{M}(x)$ is the interpretation of $x$ in $\mathbb{M}$, and $\mathbb{M}[x/a]$ is the model modified to interpret $x$ as a random variable $X$ such that $X(\eta, \rho) = a$. Note that the interpretation of a term only depends on the interpretation of its subterms for the same values of $\eta$ and $\rho$, and thus the value of $\mathbb{M}[x/a](x)$ is only relevant on $\eta, \rho$. We refer the reader to [Baelde et al. 2023] for the full details, including the interpretation of recursive definitions when they satisfy a suitable well-foundedness condition, as well as how to check that some terms do correspond to PPTM computations in order to apply cryptographic assumptions.

While it could seem more natural to have infinite tapes, rather than finite but arbitrarily long ones, this has technical motivations. It ensures that all functions computed on tapes actually correspond to random variables, i.e. that they are measurable. This restriction of our logic (and of the original CCSA logic) is not limiting when it comes to modeling cryptographic protocols and attackers, which all run in PTIME. It is however crucial that the length of tapes can grow with $\eta$. The restriction to finite tapes is standard in formal cryptographic reasoning: it is present, e.g., in approaches based on Hoare logics [Barthe et al. 2011; Petcher and Morrisett 2015; Basin et al. 2020].
## 4.2. Local and global formulas

Squirrel's logic is structured around two kinds of formulas: we call global formulas the formulas of first-order logic built around the ~ predicate, and local formulas the terms of type bool. To clearly distinguish the two, we add tildes to logical connectives and quantifiers at the global level. We also note formulas with different letters: φ and ψ for local formulas and F and G for global ones.

$$ 
\begin{align*}
F &:= F \tilde{\wedge} F' \mid F \tilde{\vee} F' \mid F \Rightarrow F' \mid \tilde{\wedge} F \mid \tilde{\vee} x.F \mid \exists x.F \mid \tilde{u} \sim \tilde{v} \mid [\phi] \mid \dots \\
\phi &:= \phi \wedge \phi' \mid \phi \vee \phi' \mid \phi \Rightarrow \phi' \mid \neg \phi \mid \forall x.\phi \mid \exists x.\phi \mid u = v \mid \dots
\end{align*}
$$

Atomic global formulas include indistinguishabilities, but also atoms of the form $[\phi]$, which can be understood as $\phi \sim \text{true}$. The syntax above is open-ended, as more predicates will be used: in addition to custom predicates introduced by the user, e.g. to model verifications on messages, we will make use of several extra predicates later in this section. Note, however, that we will not use equality at the global level.

Indistinguishability atoms $\tilde{u} \sim \tilde{v}$ can only be formed when $u_i$ and $v_i$ have the same type for all $i$. Moreover, this type must be of order at most 1, i.e. of the form $\tau_1 \to \dots \to \tau_n$ where all $\tau_k$ are base atomic types. Further, we assume that elements of base types can be encoded as bitstrings, which allows interpreting these atoms as in Section 2.2, with a generalization: we now consider a distinguisher that can access the (semantics of) terms as oracles, which can be called on arbitrary inputs to obtain new data.

As said before, local formulas are just boolean terms. As such, the syntax above should be understood as syntactic sugar: for instance, $\phi \wedge \psi$ stands for $(\wedge) \phi \psi$ where $(\wedge)$ is a constant function of type $\mathbf{bool} \to \mathbf{bool} \to \mathbf{bool}$. We also view local quantifiers in this way: $\forall(x : \tau)$. $\phi$ is a notation for $\forall_{\tau} (\lambda(x : \tau). \phi)$ where $\forall_{\tau}$ is a constant of type $(\tau \to \mathbf{bool}) \to \mathbf{bool}$. We require that all models interpret these logical constants as expected. In particular, $\llbracket \forall x. \phi \rrbracket_{\mathbb{M}}^{\eta, \rho} = 1$ iff $\llbracket \phi \rrbracket_{\mathbb{M}[x/a]}^{\eta, \rho} = 1$ for all $a \in \llbracket \tau \rrbracket_{\mathbb{M}}^{\eta}$.

**Example 4.1.** Consider once again the BASIC HASH protocol of Figure 3. Instead of expressing its security by using an equivalence, we can also state it with a local formula over the previously defined macros `input_r` and `output_r`:

$$ 
\begin{align*}
\forall i : \textbf{index.} \quad & \text{happens}(R(i)) \wedge \text{output}_r @ R(i) = \text{true} \\
& \Rightarrow \exists j : \textbf{index.} \quad T(j) < R(i) \wedge \text{input}_r @ R(i) = \text{output}_r @ T(j)
\end{align*}
$$

Asking that this formula holds with overwhelming probability properly expresses authentication for any trace: whenever some tag $R(i)$ accepts, its input value must have been produced in the past by an honest reader $T(j)$.

As usual in first-order logic, a global formula can be satisfied (or not) in a model: we write $M \models F$ when this is the case. A global formula is valid when it is satisfied in all models. We write $F \models G$ if, for all $M$, $M \models F$ implies $M \models G$. A local formula, however, is valid if it is overwhelmingly true in all models: $\phi$ is valid iff $[\phi]$ is valid, i.e. $\eta \mapsto \text{Pr}_{\rho \in T_{M,\eta}} (\llbracket \phi \rrbracket_{\mathbb{M}}^{\eta, \rho} = 1)$ is overwhelming.

**Example 4.2.** We have $[\phi \Rightarrow \psi] \models [\phi] \Rightarrow [\psi]$: if both $\phi \Rightarrow \psi$ and $\phi$ are overwhelmingly true, then so must be $\psi$. However, $[\phi] \Rightarrow [\psi] \not\models [\phi \Rightarrow \psi]$: indeed, $[\phi] \Rightarrow [\psi]$ might be satisfied in a model where $\phi$ is not overwhelmingly true, but true for half of the tapes; hence $\psi$ could be always false, and $[\phi \Rightarrow \psi]$ does not hold.

**Example 4.3.** We have $[\phi \tilde{\vee} [\psi] \models [\phi \vee \psi]$ but not the converse: there might be models where only $\phi$ holds for half of the random tapes and only $\psi$ holds for the other half, hence $\phi \vee \psi$ is overwhelmingly true (even exactly true) while neither $\phi$ nor $\psi$ is.
## 4.2. Local and global formulas

Squirrel's logic is structured around two kinds of formulas: we call global formulas the formulas of first-order logic built around the ~ predicate, and local formulas the terms of type bool. To clearly distinguish the two, we add tildes to logical connectives and quantifiers at the global level. We also note formulas with different letters: φ and ψ for local formulas and F and G for global ones.

$$F := F \tilde{\wedge} F' | F \tilde{\vee} F' | F \Rightarrow F' | \tilde{\wedge} F | \tilde{\vee} x.F | \exists x.F | \vec{u} \sim \vec{v} | [\phi] | \dots$$
$$\phi := \phi \wedge \phi' | \phi \vee \phi' | \phi \Rightarrow \phi' | \neg \phi | \forall x.\phi | \exists x.\phi | u = v | \dots$$

Atomic global formulas include indistinguishabilities, but also atoms of the form $[\phi]$, which can be understood as $\phi \sim \text{true}$. The syntax above is open-ended, as more predicates will be used: in addition to custom predicates introduced by the user, e.g. to model verifications on messages, we will make use of several extra predicates later in this section. Note, however, that we will not use equality at the global level.

Indistinguishability atoms $\vec{u} \sim \vec{v}$ can only be formed when $u_i$ and $v_i$ have the same type for all $i$. Moreover, this type must be of order at most 1, i.e. of the form $\tau_1 \to \dots \to \tau_n$ where all $\tau_k$ are base atomic types. Further, we assume that elements of base types can be encoded as bitstrings, which allows interpreting these atoms as in Section 2.2, with a generalization: we now consider a distinguisher that can access the (semantics of) terms as oracles, which can be called on arbitrary inputs to obtain new data.

As said before, local formulas are just boolean terms. As such, the syntax above should be understood as syntactic sugar: for instance, $\phi \wedge \psi$ stands for $(\wedge) \phi \psi$ where $(\wedge)$ is a constant function of type bool $\to$ bool $\to$ bool. We also view local quantifiers in this way: $\forall(x : \tau). \phi$ is a notation for $\forall_{\tau} (\lambda(x : \tau). \phi)$ where $\forall_{\tau}$ is a constant of type $(\tau \to \text{bool}) \to \text{bool}$. We require that all models interpret these logical constants as expected. In particular, $\llbracket \forall x. \phi \rrbracket_{\mathbb{M}}^{\eta, \rho} = 1$ iff $\llbracket \phi \rrbracket_{\mathbb{M}[x/a]}^{\eta, \rho} = 1$ for all $a \in \llbracket \tau \rrbracket_{\mathbb{M}}^{\eta}$.

**Example 4.1.** Consider once again the BASIC HASH protocol of Figure 3. Instead of expressing its security by using an equivalence, we can also state it with a local formula over the previously defined macros `input_r` and `output_r`:

$$\forall i : \text{index.} \quad \text{happens}(R(i)) \wedge \text{output}_r@R(i) = \text{true} \\ \Rightarrow \exists j : \text{index.} \quad T(j) < R(i) \wedge \text{input}_r@R(i) = \text{output}_r@T(j)$$

Asking that this formula holds with overwhelming probability properly expresses authentication for any trace: whenever some tag $R(i)$ accepts, its input value must have been produced in the past by an honest reader $T(j)$.

As usual in first-order logic, a global formula can be satisfied (or not) in a model: we write $M \models F$ when this is the case. A global formula is valid when it is satisfied in all models. We write $F \models G$ if, for all $M$, $M \models F$ implies $M \models G$. A local formula, however, is valid if it is overwhelmingly true in all models: $\phi$ is valid iff $[\phi]$ is valid, i.e. $\eta \mapsto \text{Pr}_{\rho \in T_{M,\eta}} (\llbracket \phi \rrbracket_{\mathbb{M}}^{\eta, \rho} = 1)$ is overwhelming.

**Example 4.2.** We have $[\phi \Rightarrow \psi] \models [\phi] \Rightarrow [\psi]$: if both $\phi \Rightarrow \psi$ and $\phi$ are overwhelmingly true, then so must be $\psi$. However, $[\phi] \Rightarrow [\psi] \not\models [\phi \Rightarrow \psi]$: indeed, $[\phi] \Rightarrow [\psi]$ might be satisfied in a model where $\phi$ is not overwhelmingly true, but true for half of the tapes; hence $\psi$ could be always false, and $[\phi \Rightarrow \psi]$ does not hold.

**Example 4.3.** We have $[\phi \tilde{\vee} [\psi] \models [\phi \vee \psi]$ but not the converse: there might be models where only $\phi$ holds for half of the random tapes and only $\psi$ holds for the other half, hence $\phi \vee \psi$ is overwhelmingly true (even exactly true) while neither $\phi$ nor $\psi$ is.
In each model, global formulas are either fixed to true or false, but their quantifiers range over random variables, i.e. elements of $RV_M(\tau)$ for some $\tau$. In contrast, local formulas are probabilistic and interpreted in $RV_M(\mathbf{bool})$, but their quantifiers range over individuals, i.e. elements $a \in [\tau]_M^{\eta, \rho}$. Despite this essential difference, we can relate quantifiers at the two levels, as shown in [Baelde et al. 2023, Proposition 2].

**PROPOSITION 4.4.** For all $\mathfrak{M}$, we have $\mathfrak{M} \models [\forall(x : \tau) . \phi]$ iff. $\mathfrak{M} \models \tilde{\forall}(x : \tau) . [\phi]$, and similarly for the existential quantifiers.

### 4.3. Proof system for global and local reasoning

Squirrel's proof system is given in a natural deduction style (though the tool's tactics are sometimes closer to sequent calculus rules) and it deals with two kinds of sequents. Global sequents are of the form $\mathcal{E}; \Theta \vdash F$ where $F$ is a global formula, $\Theta$ is a set of global formulas, and $\mathcal{E}$ is a list of typed variable declarations containing at least all free variables of $\Theta$, $F$. Such a sequent can be read as the global formula $\tilde{\forall}\mathcal{E}. (\tilde{\lambda}\Theta \Rightarrow F)$, and it is valid when the associated formula is valid. Local sequents are of the form $\mathcal{E}; \Theta; \Gamma \vdash \phi$ where $\phi$ is a local formula, $\Gamma$ is a set of local formulas, and the other components are as before, with $\mathcal{E}$ declaring all free variables of $\Theta, \Gamma$ and $\phi$. The formula associated to a local sequent is $\tilde{\forall}\mathcal{E}. (\tilde{\lambda}\Theta \Rightarrow [\wedge\Gamma \Rightarrow \phi])$.

It is important to note, in the meaning of local sequents, that the second implication happens at the local level. As a result, the global hypotheses of $\Theta$ and the local hypotheses of $\Gamma$ take a different meaning, illustrated in the following selected rules:

$$ \begin{array}{c} \mathcal{E}; \Theta, F \vdash F \\ \mathcal{E}; \Theta; \Gamma, \phi \vdash \phi \\ \mathcal{E}; \Theta, [\phi]; \Gamma \vdash \phi \\ \mathcal{E}; \Theta; \emptyset \vdash \phi \\ \mathcal{E}; \Theta \vdash [\phi] \end{array} \qquad \begin{array}{c} \mathcal{E}; \Theta; \emptyset \vdash \phi \\ \mathcal{E}; \Theta \vdash [\phi] \end{array} $$

The first rule is the usual axiom rule for the global logic. The second and third rules are local and global versions of the axiom rule for the local logic. The last rule allows proving a global sequent whose conclusion is $[\phi]$ from the corresponding local sequent.

The local equality predicate gives rise to the ability to rewrite at the local level, which is in fact a generalization of the **REWRITE** rule from Figure 2:

$$ \frac{\mathcal{E}; \Theta; \Gamma \vdash u = v \qquad \mathcal{E}; \Theta; \Gamma \vdash \phi\{x \mapsto u\} \qquad \mathcal{E}; \Theta; \Gamma \vdash \phi\{x \mapsto v\}}{\mathcal{E}; \Theta; \Gamma \vdash \phi\{x \mapsto v\}} $$

In the tool, a powerful **rewrite** tactic is provided, which builds on the previous rule as well as more basic rules, to perform various kinds of rewriting. The tactic can be invoked on a goal $\mathcal{E}; \Theta; \Gamma \vdash \phi$ to selectively replace occurrences of $u$ into $v$ inside $\Theta, \Gamma$ and $\phi$ when $u = v$ is part of the hypotheses (or can be simply derived from them). If $u = v$ is a local hypothesis, however, rewriting will only be possible in $\Gamma$ and $\phi$; rewriting in $\Theta$ requires a global hypothesis $[u = v]$, and is only possible at specific occurrences in $\Theta$.

The previous result relating global and local quantifiers justifies that our sequents only feature a top-level environment $\mathcal{E}$ corresponding to a global quantification. The rules for universal quantifiers in our proof system are as follows, assuming that $x$ does not occur in $\mathcal{E}$, and that $t$ is a well-typed term of type $\tau$ in environment $\mathcal{E}$:

$$ \frac{\mathcal{E}, x : \tau; \Theta \vdash F \qquad \mathcal{E}; \Theta \vdash \tilde{\forall}(x : \tau) . F \qquad \mathcal{E}, x : \tau; \Theta \vdash \Gamma \vdash \phi \qquad \mathcal{E}; \Theta \vdash \forall (x : \tau) . \phi}{\mathcal{E}; \Theta \vdash \tilde{\forall}(x : \tau) . F \qquad \mathcal{E}; \Theta \vdash F\{x \mapsto t\} \qquad \mathcal{E}; \Theta \vdash \Gamma \vdash \forall (x : \tau) . \phi \qquad \mathcal{E}; \Theta \vdash \Gamma \vdash \phi\{x \mapsto t\}} $$

Let us mention one last articulation between the global and local logics:

$$ \frac{\mathcal{E}; \Theta; \Gamma_1 \vdash \phi_1 \qquad \mathcal{E}; \Theta \vdash (\wedge \Gamma_0 \Rightarrow \phi_0) \sim (\wedge \Gamma_1 \Rightarrow \phi_1)}{\mathcal{E}; \Theta; \Gamma_0 \vdash \phi_0} $$
In each model, global formulas are either fixed to true or false, but their quantifiers range over random variables, i.e. elements of $RV_M(\tau)$ for some $\tau$. In contrast, local formulas are probabilistic and interpreted in $RV_M(\mathbf{bool})$, but their quantifiers range over individuals, i.e. elements $a \in [\tau]_M^{\eta, \rho}$. Despite this essential difference, we can relate quantifiers at the two levels, as shown in [Baelde et al. 2023, Proposition 2].

**PROPOSITION 4.4.** For all $\mathbb{M}$, we have $\mathbb{M} \models [\forall(x : \tau).\phi]$ iff. $\mathbb{M} \models \tilde{\forall}(x : \tau).[\phi]$, and similarly for the existential quantifiers.

### 4.3. Proof system for global and local reasoning

Squirrel's proof system is given in a natural deduction style (though the tool's tactics are sometimes closer to sequent calculus rules) and it deals with two kinds of sequents. Global sequents are of the form $\mathcal{E}; \Theta \vdash F$ where $F$ is a global formula, $\Theta$ is a set of global formulas, and $\mathcal{E}$ is a list of typed variable declarations containing at least all free variables of $\Theta$, $F$. Such a sequent can be read as the global formula $\tilde{\forall}\mathcal{E}.(\tilde{\lambda}\Theta \Rightarrow F)$, and it is valid when the associated formula is valid. Local sequents are of the form $\mathcal{E}; \Theta; \Gamma \vdash \phi$ where $\phi$ is a local formula, $\Gamma$ is a set of local formulas, and the other components are as before, with $\mathcal{E}$ declaring all free variables of $\Theta, \Gamma$ and $\phi$. The formula associated to a local sequent is $\tilde{\forall}\mathcal{E}.(\tilde{\lambda}\Theta \Rightarrow [\wedge\Gamma \Rightarrow \phi])$.

It is important to note, in the meaning of local sequents, that the second implication happens at the local level. As a result, the global hypotheses of $\Theta$ and the local hypotheses of $\Gamma$ take a different meaning, illustrated in the following selected rules:

$$ \begin{array}{ccc} \overline{\mathcal{E}; \Theta, F \vdash F} & \overline{\mathcal{E}; \Theta; \Gamma, \phi \vdash \phi} & \overline{\mathcal{E}; \Theta, [\phi]; \Gamma \vdash \phi} \\ \mathcal{E}; \Theta; \emptyset \vdash \phi & \mathcal{E}; \Theta \vdash [\phi] & \mathcal{E}; \Theta \vdash [\emptyset] \end{array} $$

The first rule is the usual axiom rule for the global logic. The second and third rules are local and global versions of the axiom rule for the local logic. The last rule allows proving a global sequent whose conclusion is $[\phi]$ from the corresponding local sequent.

The local equality predicate gives rise to the ability to rewrite at the local level, which is in fact a generalization of the **REWRITE** rule from Figure 2:

$$ \frac{\mathcal{E}; \Theta; \Gamma \vdash u = v \qquad \mathcal{E}; \Theta; \Gamma \vdash \phi\{x \mapsto u\} \qquad \mathcal{E}; \Theta; \Gamma \vdash \phi\{x \mapsto v\}}{\mathcal{E}; \Theta; \Gamma \vdash \phi\{x \mapsto v\}} $$

In the tool, a powerful **rewrite** tactic is provided, which builds on the previous rule as well as more basic rules, to perform various kinds of rewriting. The tactic can be invoked on a goal $\mathcal{E}; \Theta; \Gamma \vdash \phi$ to selectively replace occurrences of $u$ into $v$ inside $\Theta, \Gamma$ and $\phi$ when $u = v$ is part of the hypotheses (or can be simply derived from them). If $u = v$ is a local hypothesis, however, rewriting will only be possible in $\Gamma$ and $\phi$; rewriting in $\Theta$ requires a global hypothesis $[u = v]$, and is only possible at specific occurrences in $\Theta$.

The previous result relating global and local quantifiers justifies that our sequents only feature a top-level environment $\mathcal{E}$ corresponding to a global quantification. The rules for universal quantifiers in our proof system are as follows, assuming that $x$ does not occur in $\mathcal{E}$, and that $t$ is a well-typed term of type $\tau$ in environment $\mathcal{E}$:

$$ \frac{\mathcal{E}, x : \tau; \Theta \vdash F \qquad \mathcal{E}; \Theta \vdash \tilde{\forall}(x : \tau).F \qquad \mathcal{E}, x : \tau; \Theta \vdash \Gamma \vdash \phi \qquad \mathcal{E}; \Theta \vdash \forall(x : \tau).\phi}{\mathcal{E}; \Theta \vdash \tilde{\forall}(x : \tau).F \qquad \mathcal{E}; \Theta \vdash F\{x \mapsto t\} \qquad \mathcal{E}; \Theta \vdash \Gamma \vdash \forall(x : \tau).\phi \qquad \mathcal{E}; \Theta \vdash \Gamma \vdash \phi\{x \mapsto t\}} $$

Let us mention one last articulation between the global and local logics:

$$ \frac{\mathcal{E}; \Theta; \Gamma_1 \vdash \phi_1 \qquad \mathcal{E}; \Theta \vdash (\wedge\Gamma_0 \Rightarrow \phi_0) \sim (\wedge\Gamma_1 \Rightarrow \phi_1)}{\mathcal{E}; \Theta; \Gamma_0 \vdash \phi_0} $$
In the tool, this rule is made available through a convenient rewrite equiv tactic, typically used to establish local formulas when they essentially derive from indistinguishability assumptions.

**Example 4.5.** A common assumption over hash functions, stronger than EUF-CMA, states that they can be seen as pseudo-random functions (PRF): for a fresh secret key sk, an attacker cannot distinguish between $x \mapsto h(x, sk)$ and a fully random function. It notably yields in our logic that $h(0, sk), h(1, sk) \sim n, m$. Applying on both sides of the equivalence the function $\lambda x, y : \mathit{message}$. $x \neq y$, we can obtain the validity of the indistinguishability formula $h(0, sk) \neq h(1, sk) \sim n \neq m$. With this global formula and the rewrite equiv tactic, we can reduce the proof of the local sequent $\mathcal{E}; \Theta; \vdash h(0, sk) \neq h(1, sk)$ to the proof of $\mathcal{E}; \Theta; \vdash n \neq m$.

A more complete description of our proof system is given in [Baelde et al. 2023]. However, it is important to point out that the system presented in that paper (or any earlier one) is only a collection of correct rules: it does not come with any completeness or cut-elimination result. Ongoing investigations are starting to provide such proof-theoretical results, though in a propositional fragment that allows to view our two-level logic in the richer framework of modal logic.

## 4.4. Cryptographic reasoning with recursive functions

It is natural to lift cryptographic reasoning to either local or global reasoning depending on the nature of the cryptographic assumption. In the case of EUF-CMA from Section 2.3, it could become a local rule of the form:

$$ \mathbf{EUF-CMA} \frac{\mathcal{E}; \Theta; \Gamma \vdash \bigwedge_{h(u,sk) \in \mathcal{S}^h_{sk}(t,m)} (u \neq m)}{\mathcal{E}; \Theta; \Gamma \vdash h(m,sk) \neq t} \text{ sk only occurs as } h(x,sk) \text{ in } t \text{ and } m $$

Yet, now that terms contain recursive functions, the meaning of forbidding occurrences of sk is unclear: forbidden computations (e.g. a leak of a secret key) might occur deep inside the recursive functions. Further, sk may be an indexed key $k(i)$, and occurrences with distinct indices $k(j)$ for $j \neq i$ should be ignored. Checking for such indirect occurrences requires a deeper analysis of the terms involved.

**Example 4.6.** Let $k(i)$ be a name symbol indexed by an integer $i$ and representing a key, and consider the following recursive function:

$$ \text{keys} = \lambda(i : \text{index}). \text{ if } (i = 0) \text{ then empty else } \langle k(i), \text{keys}(i-1) \rangle $$

where we assume to have functions symbols for the standard operations over integers. Basically, keys($i$) computes the list $[k(i), k(i-1), \dots, k(1)]$ (encoded as nested pairs). Consider some index terms $i_0, j_0$ and assume that $j_0 < i_0$. To prove $h(\text{att}(\text{keys}(j_0)), k(i_0)) \neq t$ with EUF-CMA, we need to check, among other things, that $k(i_0)$ does not occur in keys($j_0$). The term keys($j_0$) cannot be evaluated without providing a concrete value for $j_0$. Moreover, if we attempted to directly check the condition on keys($j_0$)'s body, we would find that it contains $k(i)$ (for a bound $i$), which can a priori be equal to $k(i_0)$. To conclude here, we need to exploit the hypothesis that $j_0 < i_0$ and details on how the recursive function keys is defined. Thus, we need a more involved check exploiting additional information that cannot be directly obtained from a superficial scrutiny of the terms.

**Generalized subterms.** We therefore introduce a generalized notion of subterm, to compute an over-approximation of all the subterms that may occur during the evaluation of a recursive function, for any model and random tapes. In addition, to allow exploiting semantic information (e.g. the fact that for any $k(i)$ in keys($j$), we have $i \neq 0$), we gather
In the tool, this rule is made available through a convenient rewrite equiv tactic, typically used to establish local formulas when they essentially derive from indistinguishability assumptions.

**Example 4.5.** A common assumption over hash functions, stronger than EUF-CMA, states that they can be seen as pseudo-random functions (PRF): for a fresh secret key sk, an attacker cannot distinguish between $x \mapsto h(x, sk)$ and a fully random function. It notably yields in our logic that $h(0, sk), h(1, sk) \sim n, m$. Applying on both sides of the equivalence the function $\lambda x, y : \text{message}$. $x \neq y$, we can obtain the validity of the indistinguishability formula $h(0, sk) \neq h(1, sk) \sim n \neq m$. With this global formula and the rewrite equiv tactic, we can reduce the proof of the local sequent $\mathcal{E}; \Theta; \vdash h(0, sk) \neq h(1, sk)$ to the proof of $\mathcal{E}; \Theta; \vdash n \neq m$.

A more complete description of our proof system is given in [Baelde et al. 2023]. However, it is important to point out that the system presented in that paper (or any earlier one) is only a collection of correct rules: it does not come with any completeness or cut-elimination result. Ongoing investigations are starting to provide such proof-theoretical results, though in a propositional fragment that allows to view our two-level logic in the richer framework of modal logic.

## 4.4. Cryptographic reasoning with recursive functions

It is natural to lift cryptographic reasoning to either local or global reasoning depending on the nature of the cryptographic assumption. In the case of EUF-CMA from Section 2.3, it could become a local rule of the form:

$$ \text{EUF-CMA} \quad \frac{\mathcal{E}; \Theta; \Gamma \vdash \bigwedge_{h(u,sk) \in S_{sk}^h (t,m)} (u \neq m)}{\mathcal{E}; \Theta; \Gamma \vdash h(m,sk) \neq t} \quad \text{sk only occurs as } h(x,sk) \text{ in } t \text{ and } m $$

Yet, now that terms contain recursive functions, the meaning of forbidding occurrences of sk is unclear: forbidden computations (e.g. a leak of a secret key) might occur deep inside the recursive functions. Further, sk may be an indexed key $k(i)$, and occurrences with distinct indices $k(j)$ for $j \neq i$ should be ignored. Checking for such indirect occurrences requires a deeper analysis of the terms involved.

**Example 4.6.** Let $k(i)$ be a name symbol indexed by an integer $i$ and representing a key, and consider the following recursive function:

$$ \text{keys} = \lambda(i : \text{index}). \text{ if } (i = 0) \text{ then empty else } \langle k(i), \text{keys}(i-1) \rangle $$

where we assume to have functions symbols for the standard operations over integers. Basically, keys($i$) computes the list $[k(i), k(i-1), \dots, k(1)]$ (encoded as nested pairs). Consider some index terms $i_0, j_0$ and assume that $j_0 < i_0$. To prove $h(\text{att}(\text{keys}(j_0)), k(i_0)) \neq t$ with EUF-CMA, we need to check, among other things, that $k(i_0)$ does not occur in keys($j_0$). The term keys($j_0$) cannot be evaluated without providing a concrete value for $j_0$. Moreover, if we attempted to directly check the condition on keys($j_0$)'s body, we would find that it contains $k(i)$ (for a bound $i$), which can a priori be equal to $k(i_0)$. To conclude here, we need to exploit the hypothesis that $j_0 < i_0$ and details on how the recursive function keys is defined. Thus, we need a more involved check exploiting additional information that cannot be directly obtained from a superficial scrutiny of the terms.

**Generalized subterms.** We therefore introduce a generalized notion of subterm, to compute an over-approximation of all the subterms that may occur during the evaluation of a recursive function, for any model and random tapes. In addition, to allow exploiting semantic information (e.g. the fact that for any $k(i)$ in keys($j$), we have $i \neq 0$), we gather
together with each subterm a local formula expressing the condition under which that subterm may be computed. A generalized subterm, or occurrence, σ in a term t is a tuple (V, φ, s): s is, roughly, a subterm of t (expanding recursive definitions), V is a set of typed variables bound above s in t, and φ is the condition under which s is evaluated in t, gathered from all if conditions. We use this notion, denoted ST(t), in cryptographic rules to replace the previous conditions on syntactic subterms. For instance, a condition expressing that k(i₀) does not occur in t now instead requires that for each (V, φ, k(i)) ∈ ST(t), the formula ∀V. φ ⇒ i₀ ≠ i holds. Taking all this into account, the EUF-CMA rule finally becomes:

$$ \text{EUF-CMA} \frac{\mathcal{E}; \Theta; \Gamma \vdash \left( \bigwedge_{(V, \phi, k(i)) \in \text{ST}_h(t, m)} \forall V. \phi \Rightarrow i_0 \neq i \right) \wedge \left( \bigwedge_{(V, \phi, h(u, k(i))) \in \text{ST}(t, m)} \forall V. (\phi \wedge i_0 = i) \Rightarrow u \neq m \right)}{\mathcal{E}; \Theta; \Gamma \vdash h(m, k(i_0)) \neq t} $$

where ST_h(t, m) is ST(t, m), where we excluded occurrences of k in subterms of the form h(·, k(·)). An additional premise (omitted here) checks that t and m are computable in polynomial time.

*Making the verification effective.* As presented here, the set of occurrences in a term may be infinite: thus, we cannot generate one premise for each occurrence. To alleviate this issue, we use heuristics that help Squirrel construct a proof obligation for the user that over-approximates this infinite set in a way that makes it expressible as a single formula. We illustrate how this can be done on an example.

**Example 4.7.** Continuing Example 4.6, consider arbitrary indices i₀, j₀ such that j₀ < i₀. Recall that keys(j₀) computes the list of keys [k(j₀), ..., k(1)]. In the style described above, a condition for a rule may require us to consider all elements (V, φ, k(i)) of ST(att(keys(j₀))) (for any i) to show that i cannot be equal to i₀. There are countably many such elements, all of the form (0, j₀ ≠ 0 ∧ j₀ − 1 ≠ 0 ∧ · · · ∧ j₀ − ℓ ≠ 0, k(j₀ − ℓ)) for ℓ ∈ N. They can all be subsumed by using instead the occurrence (i, 0 < i ∧ i ≤ j₀ ⇒ i ≠ i₀, which can indeed be proved under the hypothesis that j₀ < i₀.

## 4.5. Reasoning over traces: induction and case analysis

We now clarify the interpretation of traces in this logic, and what kind of reasoning we can perform over them. Following the modeling approach outlined in Section 3, recall that we may use A : index → timestamp to represent an indexed action. Assuming for simplicity that we only have this action A, we restrict our attention to models M where

$$ [[timestamp]]_M = \{ \text{init, undef} \} \cup \{ A(n) \mid n \in N \} $$

where N is a finite subset of [[index]]_M and undef is a special value used to interpret all timestamps that do not happen. Then, the constants init and A are interpreted naturally, independently of η, ρ:

$$ [[\text{init}]]_{\mathbb{M}}^{\eta, \rho} = \text{init} \qquad [[A]]_{\mathbb{M}}^{\eta, \rho}(n) = A(n) \text{ for } n \in N \qquad [[A]]_{\mathbb{M}}^{\eta, \rho}(n) = \text{undef otherwise} $$

The following axiom is sound in this class of models:

$$ [[\forall x : \text{timestamp. happens}(x)] \Rightarrow (x = \text{init} \lor \exists i : \text{index. } x = A(i))] $$

It can effectively be used to reason by case analysis on timestamps, but only at the level of local formulas. At the global level, it is tempting to postulate a stronger axiom:

$$ \tilde{\forall} x : \text{timestamp. } [\text{happens}(x)] \Rightarrow ([x = \text{init}] \quad \tilde{\vee} \quad \exists i : \text{index. } [x = A(i)]) $$
together with each subterm a local formula expressing the condition under which that subterm may be computed. A generalized subterm, or occurrence, σ in a term t is a tuple (V, φ, s): s is, roughly, a subterm of t (expanding recursive definitions), V is a set of typed variables bound above s in t, and φ is the condition under which s is evaluated in t, gathered from all if conditions. We use this notion, denoted ST(t), in cryptographic rules to replace the previous conditions on syntactic subterms. For instance, a condition expressing that k(i₀) does not occur in t now instead requires that for each (V, φ, k(i)) ∈ ST(t), the formula ∀V. φ ⇒ i₀ ≠ i holds. Taking all this into account, the EUF-CMA rule finally becomes:

$$ \text{EUF-CMA} \quad \frac{\mathcal{E}; \Theta; \Gamma \vdash \left( \bigwedge_{(V, \phi, k(i)) \in \text{ST}_h(t, m)} \forall V. \phi \Rightarrow i_0 \neq i \right) \wedge \left( \bigwedge_{(V, \phi, h(u, k(i))) \in \text{ST}(t, m)} \forall V. (\phi \wedge i_0 = i) \Rightarrow u \neq m \right)}{\mathcal{E}; \Theta; \Gamma \vdash h(m, k(i_0)) \neq t} $$

where ST_h(t, m) is ST(t, m), where we excluded occurrences of k in subterms of the form h(·, k(·)). An additional premise (omitted here) checks that t and m are computable in polynomial time.

*Making the verification effective.* As presented here, the set of occurrences in a term may be infinite: thus, we cannot generate one premise for each occurrence. To alleviate this issue, we use heuristics that help Squirrel construct a proof obligation for the user that over-approximates this infinite set in a way that makes it expressible as a single formula. We illustrate how this can be done on an example.

**Example 4.7.** Continuing Example 4.6, consider arbitrary indices i₀, j₀ such that j₀ < i₀. Recall that keys(j₀) computes the list of keys [k(j₀), ..., k(1)]. In the style described above, a condition for a rule may require us to consider all elements (V, φ, k(i)) of ST(att(keys(j₀))) (for any i) to show that i cannot be equal to i₀. There are countably many such elements, all of the form (0, j₀ ≠ 0 ∧ j₀ − 1 ≠ 0 ∧ · · · ∧ j₀ − ℓ ≠ 0, k(j₀ − ℓ)) for ℓ ∈ N. They can all be subsumed by using instead the occurrence (i, 0 < i ∧ i ≤ j₀ ⇒ i ≠ i₀, which can indeed be proved under the hypothesis that j₀ < i₀.

## 4.5. Reasoning over traces: induction and case analysis

We now clarify the interpretation of traces in this logic, and what kind of reasoning we can perform over them. Following the modeling approach outlined in Section 3, recall that we may use A : index → timestamp to represent an indexed action. Assuming for simplicity that we only have this action A, we restrict our attention to models M where

$$ [[timestamp]]_M = \{ \text{init, undef} \} \cup \{ A(n) \mid n \in N \} $$

where N is a finite subset of [[index]]_M and undef is a special value used to interpret all timestamps that do not happen. Then, the constants init and A are interpreted naturally, independently of η, ρ:

$$ [[\text{init}]_{\mathbb{M}}^{\eta, \rho} = \text{init} \qquad [[A]_{\mathbb{M}}^{\eta, \rho}(n) = A(n) \text{ for } n \in N \qquad [[A]_{\mathbb{M}}^{\eta, \rho}(n) = \text{undef otherwise} $$

The following axiom is sound in this class of models:

$$ [[\forall x : \text{timestamp. happens}(x)] \Rightarrow (x = \text{init} \lor \exists i : \text{index. } x = A(i))] $$

It can effectively be used to reason by case analysis on timestamps, but only at the level of local formulas. At the global level, it is tempting to postulate a stronger axiom:

$$ \tilde{\forall} x : \text{timestamp. } [\text{happens}(x)] \Rightarrow ([x = \text{init}] \quad \tilde{\vee} \quad \exists i : \text{index. } [x = A(i)]) $$
However, this is too strong, and unsound in our class of models: consider for instance a random variable over timestamps that is init for some random tapes and some A(n) for other tapes. To avoid this problem, we crucially need to quantify over random variables that are actually constant, i.e. which depend neither on η nor on ρ. Assuming a global predicate const(·) with exactly this meaning, we can now write the following, which is sound in our class of models:

$$ \forall x : \mathit{timestamp}. \mathit{const}(x) \tilde{\lambda} [\mathit{happens}(x)] \Rightarrow ([x = \mathit{init}] \tilde{\nu} \exists i : \mathit{index}. [x = A(i)]) $$

In practice, such axioms are used in Squirrel proofs through the case tactic. This tactic, when given a timestamp, will perform a case analysis for local or global goals. However, when the goal is a global sequent, it will generate an additional subgoal to verify that the timestamp is constant, corresponding to the hypothesis in our axiom above. In practice, the constancy assumptions come from the target security property. For instance, the equivalence of protocols modeled in Section 3.2 would more precisely be stated as $\tilde{\forall} \tau. \mathit{const}(\tau) \Rightarrow \mathit{frame}_r @ \tau \sim \mathit{frame}_i @ \tau$.

Case analysis over timestamps is not always sufficient to prove a goal, and induction is sometimes needed. At the local level, induction is supported by the following axiom, which is obviously valid in our intended class of models:

$$ [\forall (p : \mathit{timestamp} \rightarrow \mathit{bool}). (\forall x. (\forall y. y < x \Rightarrow p y) \Rightarrow p x) \Rightarrow (\forall x. p x)] $$

At the global level, the lack of higher-order quantification forces us to resort to an axiom scheme and, more importantly, we need const(·) assumptions. For any global formula F, the following axiom is valid:

$$ (\tilde{\forall} x. \mathit{const}(x) \Rightarrow (\tilde{\forall} y. \mathit{const}(y) \tilde{\lambda} [y < x] \Rightarrow F\{x \mapsto y\}) \Rightarrow F) \Rightarrow (\tilde{\forall} x. \mathit{const}(x) \Rightarrow F) $$

Without the const(·) restrictions, the axiom would be unsound: in a nutshell, the problem is that the well-founded relation < over $[[\mathit{timestamp}]_M]$ does not lift to a well-founded relation [· < ·] over random variables. This can be generalized to arbitrary sets of actions, and to arbitrary well-founded types: one may for instance reason by induction over natural numbers or trees, along the same lines.

## 4.6. Bi-deduction & cryptographic reductions

Given the scope of the logic, the question of automating some proof steps in Squirrel was quickly raised. A key property of computational indistinguishability is that it is preserved by public computations: if $\tilde{u} \sim \tilde{v}$ holds then for any adversarially computable function $f$, we have $f(\tilde{u}) \sim f(\tilde{v})$. This property, introduced in [Baelde et al. 2022], is of particular interest for two reasons:

- it is the theoretical justification behind many cryptographic proof steps;

- it is simple, notably because it is compositional, as opposed to indistinguishability ~ which is not (see point 3 of Example 2.6).

For these reasons, this property turned-out to be a nice target for automation, reducing the proof-burden put on the user and allowing more high-level reasoning steps.

**Bi-Deduction.** Let $\sharp(\tilde{v}_0; \tilde{v}_1)$ be a pair of sequences of terms, representing the left and right scenarios of an equivalence. We say that it is bi-deducible from another pair $\sharp(\tilde{u}_0; \tilde{u}_1)$, which we write $\sharp(\tilde{u}_0; \tilde{u}_1) \triangleright \sharp(\tilde{v}_0; \tilde{v}_1)$, if there exists a simulator function $S$ that can be efficiently computed by the adversary and such that $S([\tilde{u}_i]) = [\tilde{v}_i]$ for any $i \in \{0; 1\}$. Crucially, the same simulator $S$ is used for both $i = 0$ and 1: $S$'s behavior cannot depend on $i$ as it does not know which side it is interacting with. The link
However, this is too strong, and unsound in our class of models: consider for instance a random variable over timestamps that is init for some random tapes and some A(n) for other tapes. To avoid this problem, we crucially need to quantify over random variables that are actually constant, i.e. which depend neither on η nor on ρ. Assuming a global predicate const(·) with exactly this meaning, we can now write the following, which is sound in our class of models:

$$ \forall x : \mathit{timestamp}. \mathit{const}(x) \tilde{\lambda} [\mathit{happens}(x)] \Rightarrow ([x = \mathit{init}] \tilde{\nu} \exists i : \mathit{index}. [x = A(i)]) $$

In practice, such axioms are used in Squirrel proofs through the case tactic. This tactic, when given a timestamp, will perform a case analysis for local or global goals. However, when the goal is a global sequent, it will generate an additional subgoal to verify that the timestamp is constant, corresponding to the hypothesis in our axiom above. In practice, the constancy assumptions come from the target security property. For instance, the equivalence of protocols modeled in Section 3.2 would more precisely be stated as $\tilde{\forall} \tau. \mathit{const}(\tau) \Rightarrow \mathit{frame}_r @ \tau \sim \mathit{frame}_i @ \tau$.

Case analysis over timestamps is not always sufficient to prove a goal, and induction is sometimes needed. At the local level, induction is supported by the following axiom, which is obviously valid in our intended class of models:

$$ [\forall (p : \mathit{timestamp} \to \mathit{bool}). (\forall x. (\forall y. y < x \Rightarrow p y) \Rightarrow p x) \Rightarrow (\forall x. p x)] $$

At the global level, the lack of higher-order quantification forces us to resort to an axiom scheme and, more importantly, we need const(·) assumptions. For any global formula F, the following axiom is valid:

$$ (\tilde{\forall} x. \mathit{const}(x) \Rightarrow (\tilde{\forall} y. \mathit{const}(y) \tilde{\lambda} [y < x] \Rightarrow F\{x \mapsto y\}) \Rightarrow F) \Rightarrow (\tilde{\forall} x. \mathit{const}(x) \Rightarrow F) $$

Without the const(·) restrictions, the axiom would be unsound: in a nutshell, the problem is that the well-founded relation < over $[[\mathit{timestamp}]_M]$ does not lift to a well-founded relation [· < ·] over random variables. This can be generalized to arbitrary sets of actions, and to arbitrary well-founded types: one may for instance reason by induction over natural numbers or trees, along the same lines.

## 4.6. Bi-deduction & cryptographic reductions

Given the scope of the logic, the question of automating some proof steps in Squirrel was quickly raised. A key property of computational indistinguishability is that it is preserved by public computations: if $\tilde{u} \sim \tilde{v}$ holds then for any adversarially computable function $f$, we have $f(\tilde{u}) \sim f(\tilde{v})$. This property, introduced in [Baelde et al. 2022], is of particular interest for two reasons:

- it is the theoretical justification behind many cryptographic proof steps;

- it is simple, notably because it is compositional, as opposed to indistinguishability ~ which is not (see point 3 of Example 2.6).

For these reasons, this property turned-out to be a nice target for automation, reducing the proof-burden put on the user and allowing more high-level reasoning steps.

**Bi-Deduction.** Let $\#(\tilde{v}_0; \tilde{v}_1)$ be a pair of sequences of terms, representing the left and right scenarios of an equivalence. We say that it is bi-deducible from another pair $\#(\tilde{u}_0; \tilde{u}_1)$, which we write $\#(\tilde{u}_0; \tilde{u}_1) \triangleright \#(\tilde{v}_0; \tilde{v}_1)$, if there exists a simulator function S that can be efficiently computed by the adversary and such that $S([\tilde{u}_i]) = [\tilde{v}_i]$ for any $i \in \{0; 1\}$. Crucially, the same simulator S is used for both $i = 0$ and 1: S's behavior cannot depend on i as it does not know which side it is interacting with. The link
between bi-deduction and indistinguishability is captured by the following rule:

$$ \mathbf{BIDEDUCE} \\ \frac{\#(\vec{u}_0; \vec{u}_1) \triangleright \#(\vec{v}_0; \vec{v}_1) \qquad \vec{u}_0 \sim \vec{u}_1}{\vec{v}_0 \sim \vec{v}_1} $$

Indeed, any efficient adversary A against the conclusion of this rule can be turned into an adversary B against the premise by simply composing A with the simulator S witnessing the bi-deduction premises. B is an efficient adversary as both A and S are, and it has the same advantage as A's.

The BIDEDUCE rule transforms the $\forall$ quantification over adversary of an equivalence into an $\exists$ quantification: instead of proving a property against any possible adversaries, of which there are infinitely many, it suffices to establish the existence of a program witnessing bi-deduction. Of course, this observation is not new, as this is the key idea behind all reduction-based arguments, whether it be in cryptography, computability or computational complexity. The main novelty is how we use bi-deduction as an automated entailment checker integrated in Squirrel tactics.

Rules. As already mentioned, bi-deduction is compositional, which allows decomposing bi-deductions as follows:

$$ \mathbf{BD.TUPLE} \\ \frac{\#(\vec{u}_0; \vec{u}_1) \triangleright \#(v_1; w_1) \quad \dots \quad \#(\vec{u}_0; \vec{u}_1) \triangleright \#(v_n; w_n)}{\#(\vec{u}_0; \vec{u}_1) \triangleright \#(v_1, \dots, v_n; w_1, \dots, w_n)} $$

Here are two selected (simple) bi-deduction rules:

$$ \mathbf{BD.FA} \\ \frac{\#(\vec{u}_0; \vec{u}_1) \triangleright \#(\vec{v}_0; \vec{v}_1)}{\#(\vec{u}_0; \vec{u}_1) \triangleright f(\#(\vec{v}_0; \vec{v}_1))} $$

$$ \mathbf{BD.TRANS} \\ \frac{\#(\vec{u}_0; \vec{u}_1) \triangleright \#(\vec{w}_0; \vec{w}_1)}{\#(\vec{u}_0; \vec{u}_1) \triangleright \#(\vec{v}_0; \vec{v}_1)} \qquad \frac{\#(\vec{u}_0, \vec{w}_0; \vec{u}_1, \vec{w}_1) \triangleright \#(\vec{v}_0; \vec{v}_1)}{\#(\vec{v}_0; \vec{v}_1)} $$

where common behaviors between the left and right scenarios are factorized when possible: e.g. $f(\#(\vec{v}_0; \vec{v}_1))$ denotes $\#(f(\vec{v}_0); f(\vec{v}_1))$. The BD.FA rule lets the adversary simulate the computation $f$: indeed, if $S$ computes $\#(\vec{v}_0; \vec{v}_1)$ from $\#(\vec{u}_0; \vec{u}_1)$, then $f \circ S$ computes $\#(f(\vec{v}_0); f(\vec{v}_1))$ from the same inputs. The transitivity rule BD.TRANS allows extending the input $\#(\vec{u}_0; \vec{u}_1)$ of a simulator trying to compute $\#(\vec{v}_0; \vec{v}_1)$ by any sequence $\#(\vec{w}_0; \vec{w}_1)$ that is bi-deducible from $\#(\vec{u}_0; \vec{u}_1)$.

The more interesting bi-deduction rules deal with functions (seen as oracles) and conditioned terms, for which we now present two simplified rules. Conditioned terms are written $(t | \phi)$, which denotes the pair of terms $(\phi, \text{if } \phi \text{ then } t \text{ else witness})$, where witness is a function symbol of the same type as $t$.

$$ \mathbf{BD.ORACLE} \\ \frac{\triangleright \#(t_0; t_1)}{\lambda y. \#(w_0; w_1) \triangleright \#(v_0; v_1)} \qquad \frac{\triangleright \#(\psi_0; \psi_1)}{\#((w_0 | \phi_0); (w_1 | \phi_1)) \triangleright \#((v_0 | \psi_0); (v_1 | \psi_1))} $$

$$ \mathbf{BD.COND} \\ \frac{\triangleright \#(\psi_0; \psi_1)}{\#((w_0 | \phi_0); (w_1 | \phi_1)) \triangleright \#((v_0 | \psi_0); (v_1 | \psi_1))} \qquad \frac{\triangleright \#(\psi_0 \wedge v_0 = w_0)}{\#(\psi_1 \wedge v_1 = w_1)} $$

The BD.ORACLE allows the simulator to call an oracle $\lambda y. \#(w_0; w_1)$ it received as input on any arguments $\#(t_0; t_1)$ that it can compute; the obtained terms $\#(w_0\{y \mapsto t_0\}; w_1\{y \mapsto t_1\})$ must be established, in the second proof obligation, to be equal to the wanted terms $\#(v_0; v_1)$. In BD.COND, the simulator retrieves from its inputs a conditioned term: the bi-deduction premise $\triangleright \#(\psi_0; \psi_1)$ guarantees that the simulator knows when to extract the terms from its input; and the logical premise ensures that when it does (i.e. when
between bi-deduction and indistinguishability is captured by the following rule:

$$ \begin{array}{c} \textcolor{red}{\textsf{BIDEDUCE}} \\ \frac{\#(\vec{u}_0; \vec{u}_1) \triangleright \#(\vec{v}_0; \vec{v}_1) \quad \vec{u}_0 \sim \vec{u}_1}{\vec{v}_0 \sim \vec{v}_1} \end{array} $$

Indeed, any efficient adversary $\mathcal{A}$ against the conclusion of this rule can be turned into an adversary $\mathcal{B}$ against the premise by simply composing $\mathcal{A}$ with the simulator $\mathcal{S}$ witnessing the bi-deduction premises. $\mathcal{B}$ is an efficient adversary as both $\mathcal{A}$ and $\mathcal{S}$ are, and it has the same advantage as $\mathcal{A}$'s.

The BIDEDUCE rule transforms the $\forall$ quantification over adversary of an equivalence into an $\exists$ quantification: instead of proving a property against any possible adversaries, of which there are infinitely many, it suffices to establish the existence of a program witnessing bi-deduction. Of course, this observation is not new, as this is the key idea behind all reduction-based arguments, whether it be in cryptography, computability or computational complexity. The main novelty is how we use bi-deduction as an automated entailment checker integrated in Squirrel tactics.

*Rules.* As already mentioned, bi-deduction is compositional, which allows decomposing bi-deductions as follows:

$$ \frac{\begin{array}{c} \textcolor{red}{\textsf{BD.TUPLE}} \\ \frac{\#(\vec{u}_0; \vec{u}_1) \triangleright \#(v_1; w_1) \quad \dots \quad \#(\vec{u}_0; \vec{u}_1) \triangleright \#(v_n; w_n)}{\#(\vec{u}_0; \vec{u}_1) \triangleright \#(v_1, \dots, v_n; w_1, \dots, w_n)} \end{array}}{\#(\vec{u}_0; \vec{u}_1) \triangleright \#(v_1, \dots, v_n; w_1, \dots, w_n)} $$

Here are two selected (simple) bi-deduction rules:

$$ \frac{\begin{array}{c} \textcolor{red}{\textsf{BD.FA}} \\ \frac{\#(\vec{u}_0; \vec{u}_1) \triangleright \#(\vec{v}_0; \vec{v}_1)}{\#(\vec{u}_0; \vec{u}_1) \triangleright f(\#(\vec{v}_0; \vec{v}_1))} \end{array}}{\lambda y. \#(w_0; w_1) \triangleright \#(v_0; v_1)} $$

$$ \frac{\begin{array}{c} \textcolor{red}{\textsf{BD.TRANS}} \\ \frac{\#(\vec{u}_0; \vec{u}_1) \triangleright \#(\vec{w}_0; \vec{w}_1) \quad \#(\vec{u}_0, \vec{w}_0; \vec{u}_1, \vec{w}_1) \triangleright \#(\vec{v}_0; \vec{v}_1)}{\#(\vec{u}_0; \vec{u}_1) \triangleright \#(\vec{v}_0; \vec{v}_1)} \end{array}}{\#(\vec{u}_0; \vec{u}_1) \triangleright \#(\vec{v}_0; \vec{v}_1)} $$

where common behaviors between the left and right scenarios are factorized when possible: e.g. $f(\#(\vec{v}_0; \vec{v}_1))$ denotes $\#(f(\vec{v}_0); f(\vec{v}_1))$. The BD.FA rule lets the adversary simulate the computation $f$: indeed, if $\mathcal{S}$ computes $\#(\vec{v}_0; \vec{v}_1)$ from $\#(\vec{u}_0; \vec{u}_1)$, then $f \circ \mathcal{S}$ computes $\#(f(\vec{v}_0); f(\vec{v}_1))$ from the same inputs. The transitivity rule BD.TRANS allows extending the input $\#(\vec{u}_0; \vec{u}_1)$ of a simulator trying to compute $\#(\vec{v}_0; \vec{v}_1)$ by any sequence $\#(\vec{w}_0; \vec{w}_1)$ that is bi-deductible from $\#(\vec{u}_0; \vec{u}_1)$.

The more interesting bi-deduction rules deal with functions (seen as oracles) and conditioned terms, for which we now present two simplified rules. Conditioned terms are written $(t | \phi)$, which denotes the pair of terms $(\phi$, if $\phi$ then $t$ else witness), where witness is a function symbol of the same type as $t$.

$$ \frac{\begin{array}{c} \textcolor{red}{\textsf{BD.ORACLE}} \\ \frac{\triangleright \#(t_0; t_1)}{\lambda y. \#(w_0; w_1) \triangleright \#(v_0; v_1)} \end{array}}{\begin{array}{c} \triangleright \#(w_0; w_1) \\ \vdash \left[ \begin{array}{l} w_0 \{ y \mapsto t_0 \} = v_0 \wedge \\ w_1 \{ y \mapsto t_1 \} = v_1 \end{array} \right] \\ \lambda y. \#(w_0; w_1) \triangleright \#(v_0; v_1) \end{array}} $$

$$ \frac{\begin{array}{c} \textcolor{red}{\textsf{BD.COND}} \\ \frac{\triangleright \#(\psi_0; \psi_1)}{\#((w_0 | \phi_0); (w_1 | \phi_1)) \triangleright \#((v_0 | \psi_0); (v_1 | \psi_1))} \end{array}}{\begin{array}{c} \triangleright \#(\psi_0; \psi_1) \\ \vdash \left[ \begin{array}{l} \psi_0 \Rightarrow (\phi_0 \wedge v_0 = w_0) \wedge \\ \psi_1 \Rightarrow (\phi_1 \wedge v_1 = w_1) \end{array} \right] \\ \lambda y. \#(w_0; w_1) \triangleright \#(v_0; v_1) \end{array}} $$

The BD.ORACLE allows the simulator to call an oracle $\lambda y. \#(w_0; w_1)$ it received as input on any arguments $\#(t_0; t_1)$ that it can compute; the obtained terms $\#(w_0 \{ y \mapsto t_0 \}; w_1 \{ y \mapsto t_1 \})$ must be established, in the second proof obligation, to be equal to the wanted terms $\#(v_0; v_1)$. In BD.COND, the simulator retrieves from its inputs a conditioned term: the bi-deduction premise $\triangleright \#(\psi_0; \psi_1)$ guarantees that the simulator knows when to extract the terms from its input; and the logical premise ensures that when it does (i.e. when
$\psi_0$ or $\psi_1$ holds), the extracted value $\sharp(w_0; w_1)$ is given as inputs (i.e. when $\phi_0$ or $\phi_1$ holds) and is equal to the wanted value $\sharp(v_0; v_1)$.

**Implementation.** We implemented a fully automated heuristic procedure for bi-deduction and integrated it in the **apply** tactic of Squirrel: concretely, it is used to automatically check the entailment between equivalences, e.g. $\vec{u}_0 \sim \vec{u}_1 \Rightarrow \vec{v}_0 \sim \vec{v}_1$. While this procedure is heuristic, and thus incomplete, it remains a useful tool in practice.

**Advanced bi-deduction.** Bi-deduction gives a formal framework to establish the existence of a simulator $S$ reducing an equivalence $\vec{u}_0 \sim \vec{u}_1$ to another equivalence $\vec{v}_0 \sim \vec{v}_1$. This looks very similar to the problem of applying a cryptographic assumption expressed as a pair of games $G_0 \approx G_1$ (in the style of Section 2): for example, given a target equivalence $\vec{u}_0 \sim \vec{u}_1$, does there exist $S$ such that $S^{G_i}$ computes $\vec{u}_i$ for all $i \in \{0; 1\}$? Extending bi-deduction to be able to handle cryptographic games would allow supporting new cryptographic assumptions in Squirrel's logic and implementation without having to manually design rules as we did in Section 2.3 and Section 4.4. This would drastically reduce the theoretical and programming work needed to support a new rule while limiting the risk of mistakes. Furthermore, it would allow non-expert users to add new cryptographic assumptions in Squirrel simply by writing, in user-space, the pair of games $G_0 \approx G_1$ associated to the assumptions.

Unfortunately, the simulators covered by our previous notion of bi-deduction are too restricted for this. First, they can only interact with *stateless* oracles that are provided as first-order terms of the logic. Second, they are deterministic programs: while they may receive randomly sampled values from their inputs, they cannot do random samplings themselves. This is too limiting: oracles of cryptographic games are often stateful (e.g. EUF-CMA relies on a stateful $\log L$); and the simulators justifying Squirrel's cryptographic rules must sample all the randomness that does not come from the cryptographic game. Recently, we designed and implemented in Squirrel an extended notion of bi-deduction supporting stateful oracles and probabilistic simulators [Baelde et al. 2024]. This introduces a number of interesting aspects: we equipped the bi-deduction predicate with Hoare-style pre- and post-conditions to handle game statefulness; and random sampling usage is tracked through *randomness constraints* that ensure that the constructed simulator does not directly access the game's random samplings. This approach, which showed good initial results, may become the standard way of handling cryptographic assumptions in Squirrel.

## 5. CONCLUSION

We have developed a logic based on the CCSA logic described in [Bana and Comon-Lundh 2014], along with proof systems for verifying reachability and equivalence properties within that framework. Our work demonstrates that this approach offers a straightforward, high-level strategy for conducting computer-assisted proofs of cryptographic protocols, offering asymptotic security guarantees within the computational model. This is reinforced by the development of the interactive prover Squirrel and its application across different case studies [Baelde et al. 2021; Baelde et al. 2022; Cremers et al. 2022; Baelde et al. 2024], summarized in Figure 4. The number of LoC mentioned includes both the model and the proof script. The cryptographic assumptions on which the proof relies are also indicated, as well as the security properties under study. We analyze reachability properties, namely various forms of authentication, and some equivalence-based properties, e.g. unlinkability on several RFID protocols, an anonymity property, as well as a strong form of secrecy. The case studies are divided into two blocks, with non-stateful protocols first and then stateful ones. The Squirrel prover was extended to post-quantum security proofs in [Cremers et al. 2022], the corresponding protocols with security guarantees against a quantum attacker are indicated with a $\star$.
$\psi_0$ or $\psi_1$ holds), the extracted value $\sharp(w_0; w_1)$ is given as inputs (i.e. when $\phi_0$ or $\phi_1$ holds) and is equal to the wanted value $\sharp(v_0; v_1)$.

*Implementation.* We implemented a fully automated heuristic procedure for bi-deduction and integrated it in the **apply** tactic of Squirrel: concretely, it is used to automatically check the entailment between equivalences, e.g. $\vec{u}_0 \sim \vec{u}_1 \Rightarrow \vec{v}_0 \sim \vec{v}_1$. While this procedure is heuristic, and thus incomplete, it remains a useful tool in practice.

*Advanced bi-deduction.* Bi-deduction gives a formal framework to establish the existence of a simulator $S$ reducing an equivalence $\vec{u}_0 \sim \vec{u}_1$ to another equivalence $\vec{v}_0 \sim \vec{v}_1$. This looks very similar to the problem of applying a cryptographic assumption expressed as a pair of games $G_0 \approx G_1$ (in the style of Section 2): for example, given a target equivalence $\vec{u}_0 \sim \vec{u}_1$, does there exist $S$ such that $S^{G_i}$ computes $\vec{u}_i$ for all $i \in \{0; 1\}$? Extending bi-deduction to be able to handle cryptographic games would allow supporting new cryptographic assumptions in Squirrel's logic and implementation without having to manually design rules as we did in Section 2.3 and Section 4.4. This would drastically reduce the theoretical and programming work needed to support a new rule while limiting the risk of mistakes. Furthermore, it would allow non-expert users to add new cryptographic assumptions in Squirrel simply by writing, in user-space, the pair of games $G_0 \approx G_1$ associated to the assumptions.

Unfortunately, the simulators covered by our previous notion of bi-deduction are too restricted for this. First, they can only interact with *stateless* oracles that are provided as first-order terms of the logic. Second, they are deterministic programs: while they may receive randomly sampled values from their inputs, they cannot do random samplings themselves. This is too limiting: oracles of cryptographic games are often stateful (e.g. EUF-CMA relies on a stateful $\log L$); and the simulators justifying Squirrel's cryptographic rules must sample all the randomness that does not come from the cryptographic game. Recently, we designed and implemented in Squirrel an extended notion of bi-deduction supporting stateful oracles and probabilistic simulators [Baelde et al. 2024]. This introduces a number of interesting aspects: we equipped the bi-deduction predicate with Hoare-style pre- and post-conditions to handle game statefulness; and random sampling usage is tracked through *randomness constraints* that ensure that the constructed simulator does not directly access the game's random samplings. This approach, which showed good initial results, may become the standard way of handling cryptographic assumptions in Squirrel.

## 5. CONCLUSION

We have developed a logic based on the CCSA logic described in [Bana and Comon-Lundh 2014], along with proof systems for verifying reachability and equivalence properties within that framework. Our work demonstrates that this approach offers a straightforward, high-level strategy for conducting computer-assisted proofs of cryptographic protocols, offering asymptotic security guarantees within the computational model. This is reinforced by the development of the interactive prover Squirrel and its application across different case studies [Baelde et al. 2021; Baelde et al. 2022; Cremers et al. 2022; Baelde et al. 2024], summarized in Figure 4. The number of LoC mentioned includes both the model and the proof script. The cryptographic assumptions on which the proof relies are also indicated, as well as the security properties under study. We analyze reachability properties, namely various forms of authentication, and some equivalence-based properties, e.g. unlinkability on several RFID protocols, an anonymity property, as well as a strong form of secrecy. The case studies are divided into two blocks, with non-stateful protocols first and then stateful ones. The Squirrel prover was extended to post-quantum security proofs in [Cremers et al. 2022], the corresponding protocols with security guarantees against a quantum attacker are indicated with a $\star$.
<table><caption>Fig. 4. Some results obtained with the Squirrel prover on various protocols.</caption><thead><tr><th>Protocol name</th><th>LoC</th><th>Assumptions</th><th>Security Properties</th></tr></thead><tbody><tr><td>Basic Hash *</td><td>100</td><td>PRF, EUF</td><td>auth. & unlinkability</td></tr><tr><td>Hash Lock *</td><td>130</td><td>PRF, EUF</td><td>auth. & unlinkability</td></tr><tr><td>LAK (with pairs) *</td><td>250</td><td>PRF, EUF</td><td>auth. & unlinkability</td></tr><tr><td>MW *</td><td>300</td><td>PRF, EUF, XOR</td><td>auth. & unlinkability</td></tr><tr><td>Feldhofer *</td><td>270</td><td>ENC-KP, INT-CTXT</td><td>auth. & unlinkability</td></tr><tr><td>Private authentication *</td><td>100</td><td>CCA<sub>1</sub>, ENC-KP</td><td>anonymity</td></tr><tr><td>Private authentication</td><td>100</td><td>CCA<sub>$</sub></td><td>anonymity</td></tr><tr><td>Signed DDH [ISO 9798-3]</td><td>240</td><td>EUF, DDH</td><td>auth. & strong secrecy</td></tr><tr><td>IKEV1<sub>PSK</sub> *</td><td>850</td><td>PRF</td><td>auth. & strong secrecy</td></tr><tr><td>IKEV2<sup>SIGN</sup><sub>PSK</sub> *</td><td>300</td><td>PRF, EUF</td><td>auth. & strong secrecy</td></tr><tr><td>BCGNP *</td><td>355</td><td>PRF, CCA<sub>1</sub>, XOR</td><td>strong secrecy</td></tr><tr><td>FSXY *</td><td>620</td><td>PRF, CCA<sub>1</sub>, XOR</td><td>strong secrecy</td></tr><tr><td>SC-AKE *</td><td>745</td><td>PRF, EUF, CCA<sub>1</sub>, XOR</td><td>auth. & strong secrecy</td></tr><tr><td>CANAuth</td><td>450</td><td>EUF</td><td>auth.</td></tr><tr><td>SLK06</td><td>80</td><td>EUF</td><td>auth.</td></tr><tr><td>YPLRK05</td><td>160</td><td>EUF</td><td>auth.</td></tr><tr><td>OSK (without reader)</td><td>320</td><td>ROM</td><td>strong secrecy</td></tr><tr><td>OSK</td><td>370</td><td>EUF</td><td>auth.</td></tr><tr><td>YubiKey</td><td>270</td><td>INT-CTXT</td><td>auth.</td></tr><tr><td>YubiHSM</td><td>720</td><td>CCA<sub>1</sub>, INT-CTXT</td><td>auth.</td></tr></tbody></table>

*Ongoing and Future Work.* As explained in Section 3, the Squirrel tool allows cryptographic protocols to be described in a process algebra, whereas the translation from protocols to the logic relies on the definition of mutually recursive functions modeling the protocol observables depending on the execution trace. To ease formal proofs, this translation does not follow the granularity of elementary execution steps in the process algebra. Instead, it groups together elementary steps in blocks following specific patterns. Whereas the soundness of the translation is easy to obtain for a simple class of protocols, some works remain to be done for more complex protocols.

We also aim to improve the automation of the prover. One option is to discharge parts of the proof that do not rely on any cryptographic assumption to SMT solvers. Another option is to rely on type systems: techniques based on typing have mainly been used in symbolic models, but we are currently working to develop such a system to obtain computational guarantees in the CCSA framework.

We aim to extend the scope of the post-quantum work initiated in [Cremers et al. 2022] and to analyze hybrid post-quantum protocols that rely on a combination of asymmetric post-quantum algorithms with well-known and well-studied pre-quantum asymmetric cryptography, e.g. based on the discrete logarithm problem.

Lastly, as mentioned in Section 3, the current notion of security in Squirrel differs from the standard one in the computational model, as the number of sessions we consider is arbitrary but fixed, in the sense that it does not depend on the security parameter. We plan to overcome this limitation, notably by leveraging the composition result outlined in [Comon et al. 2020]. Furthermore, we intend to expand on our methodology to go beyond asymptotic guarantees and provide concrete security bounds.

## ACKNOWLEDGMENTS

This work received funding from the France 2030 program managed by the French National Research Agency under grant agreement No. ANR-22-PECY-0006.
<table><caption>Fig. 4. Some results obtained with the Squirrel prover on various protocols.</caption><thead><tr><th>Protocol name</th><th>LoC</th><th>Assumptions</th><th>Security Properties</th></tr></thead><tbody><tr><td>Basic Hash *</td><td>100</td><td>PRF, EUF</td><td>auth. & unlinkability</td></tr><tr><td>Hash Lock *</td><td>130</td><td>PRF, EUF</td><td>auth. & unlinkability</td></tr><tr><td>LAK (with pairs) *</td><td>250</td><td>PRF, EUF</td><td>auth. & unlinkability</td></tr><tr><td>MW *</td><td>300</td><td>PRF, EUF, XOR</td><td>auth. & unlinkability</td></tr><tr><td>Feldhofer *</td><td>270</td><td>ENC-KP, INT-CTXT</td><td>auth. & unlinkability</td></tr><tr><td>Private authentication *</td><td>100</td><td>CCA<sub>1</sub>, ENC-KP</td><td>anonymity</td></tr><tr><td>Private authentication</td><td>100</td><td>CCA<sub>$</sub></td><td>anonymity</td></tr><tr><td>Signed DDH [ISO 9798-3]</td><td>240</td><td>EUF, DDH</td><td>auth. & strong secrecy</td></tr><tr><td>IKEV1<sub>PSK</sub> *</td><td>850</td><td>PRF</td><td>auth. & strong secrecy</td></tr><tr><td>IKEV2<sup>SIGN</sup><sub>PSK</sub> *</td><td>300</td><td>PRF, EUF</td><td>auth. & strong secrecy</td></tr><tr><td>BCGNP *</td><td>355</td><td>PRF, CCA<sub>1</sub>, XOR</td><td>strong secrecy</td></tr><tr><td>FSXY *</td><td>620</td><td>PRF, CCA<sub>1</sub>, XOR</td><td>strong secrecy</td></tr><tr><td>SC-AKE *</td><td>745</td><td>PRF, EUF, CCA<sub>1</sub>, XOR</td><td>auth. & strong secrecy</td></tr><tr><td>CANAuth</td><td>450</td><td>EUF</td><td>auth.</td></tr><tr><td>SLK06</td><td>80</td><td>EUF</td><td>auth.</td></tr><tr><td>YPLRK05</td><td>160</td><td>EUF</td><td>auth.</td></tr><tr><td>OSK (without reader)</td><td>320</td><td>ROM</td><td>strong secrecy</td></tr><tr><td>OSK</td><td>370</td><td>EUF</td><td>auth.</td></tr><tr><td>YubiKey</td><td>270</td><td>INT-CTXT</td><td>auth.</td></tr><tr><td>YubiHSM</td><td>720</td><td>CCA<sub>1</sub>, INT-CTXT</td><td>auth.</td></tr></tbody></table>

*Ongoing and Future Work.* As explained in Section 3, the Squirrel tool allows cryptographic protocols to be described in a process algebra, whereas the translation from protocols to the logic relies on the definition of mutually recursive functions modeling the protocol observables depending on the execution trace. To ease formal proofs, this translation does not follow the granularity of elementary execution steps in the process algebra. Instead, it groups together elementary steps in blocks following specific patterns. Whereas the soundness of the translation is easy to obtain for a simple class of protocols, some works remain to be done for more complex protocols.

We also aim to improve the automation of the prover. One option is to discharge parts of the proof that do not rely on any cryptographic assumption to SMT solvers. Another option is to rely on type systems: techniques based on typing have mainly been used in symbolic models, but we are currently working to develop such a system to obtain computational guarantees in the CCSA framework.

We aim to extend the scope of the post-quantum work initiated in [Cremers et al. 2022] and to analyze hybrid post-quantum protocols that rely on a combination of asymmetric post-quantum algorithms with well-known and well-studied pre-quantum asymmetric cryptography, e.g. based on the discrete logarithm problem.

Lastly, as mentioned in Section 3, the current notion of security in Squirrel differs from the standard one in the computational model, as the number of sessions we consider is arbitrary but fixed, in the sense that it does not depend on the security parameter. We plan to overcome this limitation, notably by leveraging the composition result outlined in [Comon et al. 2020]. Furthermore, we intend to expand on our methodology to go beyond asymptotic guarantees and provide concrete security bounds.

## ACKNOWLEDGMENTS

This work received funding from the France 2030 program managed by the French National Research Agency under grant agreement No. ANR-22-PECY-0006.
REFERENCES

David Baelde, Stéphanie Delaune, Charlie Jacomme, Adrien Koutsos, and Solène Moreau. 2021. An Interac-
tive Prover for Protocol Verification in the Computational Model. In *42nd IEEE Symposium on Security
and Privacy*, SP 2021, San Francisco, CA, USA, *24-27 May 2021*. IEEE, 537–554.

David Baelde, Stéphanie Delaune, Adrien Koutsos, and Solène Moreau. 2022. Cracking the Stateful Nut: Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant. In *35th IEEE Computer Security Foundations Symposium, CSF 2022, Haifa, Israel, August 7-10, 2022*. IEEE, 289–304.

David Baelde, Adrien Koutsos, and Joseph Lallemand. 2023. A Higher-Order Indistinguishability Logic for Cryptographic Reasoning. In *38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023*. 1–13.

David Baelde, Adrien Koutsos, and Justine Sauvage. 2024. Cryptographic Reductions By Bi-Deduction. (March 2024). https://hal.science/hal-04511718

Gergei Bana and Hubert Comon-Lundh. 2012. Towards Unconditional Soundness: Computationally Complete Symbolic Attacker. In *Principles of Security and Trust - First International Conference, POST 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012, Proceedings (Lecture Notes in Computer Science)*, Pierpaolo Degano and Joshua D. Guttman (Eds.), Vol. 7215. Springer, 189–208.

Gergei Bana and Hubert Comon-Lundh. 2014. A Computationally Complete Symbolic Attacker for Equiva-
lence Properties. In *Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications
Security, Scottsdale, AZ, USA, November 3-7, 2014*. ACM, 609–620.

Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, and Bryan Parno. 2021. SoK: Computer-Aided Cryptography. In *42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24-27 May 2021*. IEEE, 777–795.

Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. 2009. Formal certification of code-based cryptographic proofs. In *Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009, Zhong Shao and Benjamin C. Pierce (Eds.). ACM, 90–101.*

Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, and Santiago Zanella Béguelin. 2011. Computer-Aided Security Proofs for the Working Cryptographer. In *Advances in Cryptology - CRYPTO 2011 - 31st Annual Cryptology Conference, Santa Barbara, CA, USA, August 14-18, 2011. Proceedings (Lecture Notes in Computer Science)*, Phillip Rogaway (Ed.), Vol. 6841. Springer, 71–90.

David A. Basin, Andreas Lochbihler, and S. Reza Sefidgar. 2020. CryptHOL: Game-Based Proofs in Higher-Order Logic. *J. Cryptol.* 33, 2 (2020), 494–566.

Bruno Blanchet. 2001. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In *14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), 11-13 June 2001, Cape Breton, Nova Scotia, Canada*. IEEE Computer Society, 82–96.

Bruno Blanchet. 2008. A Computationally Sound Mechanized Prover for Security Protocols. *IEEE Trans. Dependable Secur. Comput.* 5, 4 (2008), 193–207.

Mayla Brusò, Konstantinos Chatzikokolakis, and Jerry den Hartog. 2010. Formal Verification of Privacy for RFID Systems. In *23rd IEEE Computer Security Foundations Symposium, CSF 2010, Edinburgh, United Kingdom, July 17-19, 2010*. IEEE Computer Society, 75–88.

Hubert Comon, Charlie Jacomme, and Guillaume Sicërri. 2020. Oracle Simulation: A Technique for Protocol Composition with Long Term Shared Secrets. In *2020 ACM SIGSAC Conference on Computer and Communications Security, CCS 2020*. ACM, 1427–1444.

Cas Cremers, Caroline Fontaine, and Charlie Jacomme. 2022. A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols. In *43rd IEEE Symposium on Security and Privacy, SP 2022, San Francisco, CA, USA, May 22-26, 2022*. IEEE, 125–141.

Danny Dolev and Andrew Chi-Chih Yao. 1981. On the Security of Public Key Protocols (Extended Abstract). In *22nd Annual Symposium on Foundations of Computer Science, Nashville, Tennessee, USA, 28-30 October 1981*. IEEE Computer Society, 350–357.

Simon Meier, Benedikt Schmidt, Cas Cremers, and David A. Basin. 2013. The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In *Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings (Lecture Notes in Computer Science)*, Natasha Sharygina and Helmut Veith (Eds.), Vol. 8044. Springer, 696–701.

Adam Petcher and Greg Morrisett. 2015. The Foundational Cryptography Framework. In *Principles of Security and Trust - 4th International Conference, POST 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings (Lecture Notes in Computer Science)*, Riccardo Focardi and Andrew C. Myers (Eds.), Vol. 9036. Springer, 53–72.
REFERENCES

David Baelde, Stéphanie Delaune, Charlie Jacomme, Adrien Koutsos, and Solène Moreau. 2021. An Interac-
tive Prover for Protocol Verification in the Computational Model. In *42nd IEEE Symposium on Security
and Privacy, SP 2021, San Francisco, CA, USA, 24-27 May 2021*. IEEE, 537–554.

David Baelde, Stéphanie Delaune, Adrien Koutsos, and Solène Moreau. 2022. Cracking the Stateful Nut: Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant. In *35th IEEE Computer Security Foundations Symposium, CSF 2022, Haifa, Israel, August 7-10, 2022*. IEEE, 289–304.

David Baelde, Adrien Koutsos, and Joseph Lallemand. 2023. A Higher-Order Indistinguishability Logic for Cryptographic Reasoning. In *38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023*. 1–13.

David Baelde, Adrien Koutsos, and Justine Sauvage. 2024. Cryptographic Reductions By Bi-Deduction. (March 2024). https://hal.science/hal-04511718

Gergei Bana and Hubert Comon-Lundh. 2012. Towards Unconditional Soundness: Computationally Complete Symbolic Attacker. In *Principles of Security and Trust - First International Conference, POST 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012, Proceedings (Lecture Notes in Computer Science)*, Pierpaolo Degano and Joshua D. Guttman (Eds.), Vol. 7215. Springer, 189–208.

Gergei Bana and Hubert Comon-Lundh. 2014. A Computationally Complete Symbolic Attacker for Equiva-
lence Properties. In *Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications
Security, Scottsdale, AZ, USA, November 3-7, 2014*. ACM, 609–620.

Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, and Bryan Parno. 2021. SoK: Computer-Aided Cryptography. In *42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24-27 May 2021*. IEEE, 777–795.

Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. 2009. Formal certification of code-based cryptographic proofs. In *Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009, Zhong Shao and Benjamin C. Pierce (Eds.). ACM, 90–101.*

Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, and Santiago Zanella Béguelin. 2011. Computer-Aided Security Proofs for the Working Cryptographer. In *Advances in Cryptology - CRYPTO 2011 - 31st Annual Cryptology Conference, Santa Barbara, CA, USA, August 14-18, 2011. Proceedings (Lecture Notes in Computer Science)*, Phillip Rogaway (Ed.), Vol. 6841. Springer, 71–90.

David A. Basin, Andreas Lochbihler, and S. Reza Sefidgar. 2020. CryptHOL: Game-Based Proofs in Higher-Order Logic. *J. Cryptol.* 33, 2 (2020), 494–566.

Bruno Blanchet. 2001. An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In *14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), 11-13 June 2001, Cape Breton, Nova Scotia, Canada*. IEEE Computer Society, 82–96.

Bruno Blanchet. 2008. A Computationally Sound Mechanized Prover for Security Protocols. *IEEE Trans. Dependable Secur. Comput.* 5, 4 (2008), 193–207.

Mayla Brusò, Konstantinos Chatzikokolakis, and Jerry den Hartog. 2010. Formal Verification of Privacy for RFID Systems. In *23rd IEEE Computer Security Foundations Symposium, CSF 2010, Edinburgh, United Kingdom, July 17-19, 2010*. IEEE Computer Society, 75–88.

Hubert Comon, Charlie Jacomme, and Guillaume Sicërri. 2020. Oracle Simulation: A Technique for Protocol Composition with Long Term Shared Secrets. In *2020 ACM SIGSAC Conference on Computer and Communications Security, CCS 2020*. ACM, 1427–1444.

Cas Cremers, Caroline Fontaine, and Charlie Jacomme. 2022. A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols. In *43rd IEEE Symposium on Security and Privacy, SP 2022, San Francisco, CA, USA, May 22-26, 2022*. IEEE, 125–141.

Danny Dolev and Andrew Chi-Chih Yao. 1981. On the Security of Public Key Protocols (Extended Abstract). In *22nd Annual Symposium on Foundations of Computer Science, Nashville, Tennessee, USA, 28-30 October 1981*. IEEE Computer Society, 350–357.

Simon Meier, Benedikt Schmidt, Cas Cremers, and David A. Basin. 2013. The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In *Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings (Lecture Notes in Computer Science)*, Natasha Sharygina and Helmut Veith (Eds.), Vol. 8044. Springer, 696–701.

Adam Petcher and Greg Morrisett. 2015. The Foundational Cryptography Framework. In *Principles of Security and Trust - 4th International Conference, POST 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings (Lecture Notes in Computer Science)*, Riccardo Focardi and Andrew C. Myers (Eds.), Vol. 9036. Springer, 53–72.
Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, and Santiago Zanella Béguelin. 2016. Dependent types and multi-monadic effects in F. In *43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016*, Rastislav Bodík and Rupak Majumdar (Eds.). ACM, 256–270.
Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, and Santiago Zanella Béguelin. 2016. Dependent types and multi-monadic effects in F. In *43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016*, Rastislav Bodík and Rupak Majumdar (Eds.). ACM, 256–270.