$$
\begin{array}{l}
\text{G.PRF}' \\
\quad \mathcal{E}; \Theta; \emptyset \vdash_{\text{pptm}} \vec{u}, m, t \qquad \mathcal{E}; \Theta \vdash \text{const}(t) \qquad \mathcal{E}; \Theta; \emptyset \vdash \psi_{\text{key}}^{k}(\vec{u}, m, t) \\
\quad \mathcal{E}; \Theta \vdash \vec{u}, (\text{hash } m (\text{k } t)) \sim \vec{u}, \text{ if } \psi_{\text{msg}}^{k}(\vec{u}, m, t) \text{ then } n_{\text{fresh}} () \text{ else hash } m (\text{k } t)
\end{array}
$$

<caption>Figure 11. Variant PRF rule.</caption>

chance of distinguishing a randomly sampled value (in the
appropriate space) from the hash of a message that has not
been used in a query to the hashing oracle.

To model this assumption, we assume the following decla-
ration, for some types key and hash:

$$
\text{hash} : \text{message} \to \text{key} \to \text{hash}
$$

We further assume a name $k : \tau \to$ key that will be used to
model the key generation mechanism of our hash function.

In order to reflect the computations with a hash oracle, we
adapt the generalised subterms, similarly to what we did for
EUF-CMA, this time with the following key defining equation:

$$
\mathcal{S}T_{\mathcal{E},k,t}^{\text{prf}}(\text{hash } m (\text{k } t')) \stackrel{\text{def}}{=} \{(\epsilon, \text{true}, m), (\epsilon, \text{true}, t')\} \cup [t \neq t'] \mathcal{S}T_{\mathcal{E},k,t}^{\text{prf}}(\text{k } t')
$$

The following rule captures the PRF assumption, i.e. it is
sound w.r.t. the class of models where hash is interpreted as a
hash function that satisfies the PRF assumption:

$$
\begin{array}{l}
\text{G.PRF} \\
\quad \mathcal{E}; \Theta; \emptyset \vdash_{\text{pptm}} \vec{u}, m, t \\
\quad \mathcal{E}; \Theta \vdash \text{const}(t) \qquad \mathcal{E}; \Theta; \emptyset \vdash \psi_{\text{key}}^{k}(\vec{u}, m, t) \wedge \psi_{\text{msg}}^{k}(\vec{u}, m, t) \\
\quad \mathcal{E}; \Theta \vdash \vec{u}, (\text{hash } m (\text{k } t)) \sim \vec{u}, (n_{\text{fresh}}())
\end{array}
$$

where $n_{\text{fresh}} : \text{unit} \to \text{hash}$ is a name that does not occur
anywhere else in the rule and the local formulas
$\psi_{\text{key}}^k(\vec{u}, m, t)$
and $\psi_{\text{msg}}^k(\vec{u}, m, t)$ satisfy the following conditions for any $\mathcal{M} \models$
$\Theta$:

* If $[\psi_{\text{key}}^k(\vec{u}, m, t)]_{\mathcal{M}:\mathcal{E}}^{\eta, \rho} = 1$ then $[\forall \vec{\alpha}. \psi \Rightarrow t \neq t_0]_{\mathcal{M}:\mathcal{E}}^{\eta, \rho} = 1$ for every $(\vec{\alpha}, \psi, k \ t_0) \in \mathcal{S}T_{\mathcal{E},k,t}^{\text{prf}}(\vec{u}, m, t)$.

* If $[\psi_{\text{msg}}^k(\vec{u}, m, t)]_{\mathcal{M}:\mathcal{E}}^{\eta, \rho} = 1$ then
  $[\forall \vec{\alpha}. \psi \Rightarrow (t = t_0) \Rightarrow (m \neq m_0)]_{\mathcal{M}:\mathcal{E}}^{\eta, \rho} = 1$
  for every $(\vec{\alpha}, \psi, \text{hash } m_0 (\text{k } t_0)) \in \mathcal{S}T_{\mathcal{E},k,t}^{\text{prf}}(\vec{u}, m, t)$.

We sketch the soundness argument of our rule. Assume, by contradiction, that the rule does not hold, i.e. consider a model $\mathcal{M}$ for which the premises are satisfied, such that $\mathcal{M} \models \Theta$ but $\mathcal{M}$ does not satisfy the equivalence in conclusion. In other words, there exists a PPTM $\mathcal{D}$ that can distinguish $[\vec{u}, \text{hash } m (\text{k } t)]_{\mathcal{M}:\mathcal{E}}^{\eta, \rho}$ from $[\vec{u}, n_{\text{fresh}} ()]_{\mathcal{M}:\mathcal{E}}^{\eta, \rho}$ with non-negligible advantage.

We construct a PRF adversary as follows:

1) First compute $[\vec{u}]_{M:\mathcal{E}}^{\eta,\rho}$ and $[m]_{M:\mathcal{E}}^{\eta,\rho}$, similarly to how it is done in the previous section for EUF-CMA. In particular, never access $k$ at index $t$, and use the hashing oracle to compute the interpretation of subterms (hash $m_0$ ($k$ $t_0$)) when $t_0$ interprets into $[t]_{M:\mathcal{E}}^{\eta,\rho}$.

2) Query the PRF challenge oracle with $[m]_{M:\mathcal{E}}^{\eta,\rho}$. Call $c$ the resulting value: in the left game, $c$ is $[\text{hash } m (\text{k } t)]_{M:\mathcal{E}}^{\eta,\rho}$; in the right game, it is $n_{\text{fresh}}$().

3) Call $\mathcal{D}$ with $([\vec{u}]_{M:\mathcal{E}}^{\eta,\rho}, c)$.

As before, our game is an equivalent reformulation of the
cryptographers’ game in the CCSA framework: we use k at
a specific index to model the key sampled by the game (and
make sure that this key is not accessed by the adversary); we
use $n_{\text{fresh}}$ to model the value sampled in the challenge (and
guarantee, again, that this source of randomness is not used
elsewhere).

In general, the first step of our PRF adversary may fail,
in case the interpretation of the terms forces an access to
$[\text{k } t]_{M:\mathcal{E}}^{\eta,\rho}$ outside of oracle computations. However, this only
happens with negligible probability because $\psi_{\text{key}}^k(\vec{u}, m, t)$ is
overwhelming.

Our PRF adversary may query the PRF challenge with an
invalid message $m$, if it has been previously used in a hash
oracle query. Again, this can only happen with negligible
probability, because $\psi_{\text{msg}}^k(\vec{u}, m, t)$ is overwhelming,

Hence the advantage of our PRF adversary is negligibly
close to the advantage of $\mathcal{D}$, which is non-negligible: we
have contradicted the PRF cryptographic assumption on the
interpretation of hash.

D. CCA Rule

In this section, we present the proof rule encoding the
IND-CCA-1 assumption, used to reason about the secrecy of
encrypted messages.

We present here the rule for the case of (randomised)
asymmetric encryption, i.e. encryption schemes using a public
encryption key, and a different, private decryption key. The case
of symmetric encryption, where the encryption and decryption
key are the same, is similar, as discussed at the end of the
section.

Assume $\mathcal{E}$ contains symbols pk, aenc, adec, modelling resp.
the public key associated to a private key, the encryption of
a message with a random value and a public key, and the
decryption of a ciphertext with a private key, with types

$$
\begin{align*}
\text{pk} : \text{key} \to \text{pubkey} \\
\text{aenc} : \text{message} \to \text{rand} \to \text{pubkey} \to \text{ciphertext} \\
\text{adec} : \text{ciphertext} \to \text{key} \to \text{message}
\end{align*}
$$

Their expected behaviour when correctly used is described
by the axiom:

$$
[\forall m : \text{message}, r : \text{rand}, k : \text{key.} \\
\qquad \text{adec} (\text{aenc } m r (\text{pk } k)) k = m]
$$

We will also assume functions len : message → int and
zero : int → message. We consider models where len m
returns the length of the bit-string interpreting m, and zero n
returns a bit-string consisting of n zeros.
The (non-adaptive) *Indistinguishability under Chosen Ciphertext Attacks* (IND-CCA-1) assumption [28] is a standard cryptographic hypothesis, stating that an adversary cannot distinguish the encryption of a message *m* from the encryption of a string of len *m* zeros, i.e. zero (len *m*); even when given access to the public encryption key, and restricted access to a decryption oracle. More precisely, for randomly sampled *k* and *r*, an adversary given access to pk and to a decryption oracle returning the decryption of any ciphertext with *k* is asked to produce a message *m* of his choice. He is then provided by a so-called “left-or-right” encryption oracle (which may only be called once) with either *aenc* *m* or *pk* or *aenc* (zero (len *m*)) or *pk*. He can afterwards no longer call the decryption oracle, and is asked to guess which ciphertext has been returned. The assumption is that such an attacker cannot do so with a non-negligible advantage.

We capture this assumption, for two distinct indexed names
$r$ and $k$, by the rule

G.CCA1

$$
\begin{align*}
& \mathcal{E}; \Theta; \emptyset \vdash_{\text{pptm}} \vec{u}, m, t_r, t_k \\
& \mathcal{E}; \Theta \vdash \text{const}(t_r) \qquad \mathcal{E}; \Theta \vdash \text{const}(t_k) \\
& \mathcal{E}; \Theta \vdash [\phi_{\text{key}}^{\text{k}}(\vec{u}, m, t_r, t_k) \wedge \phi_{\text{rand}}^{\text{r}}(\vec{u}, m, t_r, t_k)] \\
& \frac{}{\mathcal{E}; \Theta \vdash \quad \begin{array}{@{}l@{}} \vec{u}, \text{ aenc } m \text{ (r } t_r \text{) (pk (k } t_k \text{))} \\ \sim \vec{u}, \text{ aenc (zero (len } m \text{)) (r } t_r \text{) (pk (k } t_k \text{))} \end{array}}
\end{align*}
$$

where $\phi_{\text{key}}^{\text{k}}(\vec{u}, m, t_r, t_k)$ and $\phi_{\text{rand}}^{\text{r}}(\vec{u}, m, t_r, t_k)$ are, similarly
to the case of L.EUF, any formulas that imply, respectively

* the correct use of the key $k$ $t_k$: the adversary only has access to the public key and the decryption oracle, meaning that $k$ $t_k$ may only appear in $pk$ ($k$ $t_k$) or $adec$ ($k$ $t_k$);

* the correct use of the randomness $r$ $t_r$: this random value is sampled by the left-or-right encryption oracle, and thus may not appear anywhere else.

Basically, under these conditions, the challenge ciphertexts
encrypting *m* or zeros cannot be distinguished (even put
together with any vector of terms *u*̃ that also satisfy the
conditions).

As in the case of rule L.EUF, to formalise these conditions,
we need to adapt the notion of generalised subterms to
account for the oracles. We define $\mathcal{ST}_{\mathcal{E},k,t_k}^{\text{cca}}(v)$ recursively just
like $\mathcal{ST}_{\mathcal{E}}(v)$ (Fig. 1), with exceptions when $v$ is a function
application:

$$
\begin{align*}
\mathcal{ST}_{\mathcal{E},k,t_k}^{\text{cca}} (\text{pk } (k \ t_0)) &\stackrel{\text{def}}{=} \\
& \phantom{=} \{ (\epsilon, \text{true}, \text{pk } (k \ t_0)), (\epsilon, \text{true}, \text{pk}) \} \\
& \phantom{=} \cup \mathcal{ST}_{\mathcal{E},k,t_k}^{\text{cca}} (t_0) \cup [t_0 \neq t_k] \mathcal{ST}_{\mathcal{E},k,t_k}^{\text{cca}} (k \ t_0) \\[1em]
\mathcal{ST}_{\mathcal{E},k,t_k}^{\text{cca}} (\text{adec } t_1 \ (k \ t_0)) &\stackrel{\text{def}}{=} \\
& \phantom{=} \{ (\epsilon, \text{true}, \text{adec } t_1 \ (k \ t_0)), (\epsilon, \text{true}, \text{adec}) \} \\
& \phantom{=} \cup \mathcal{ST}_{\mathcal{E},k,t_k}^{\text{cca}} (t_0) \cup \mathcal{ST}_{\mathcal{E},k,t_k}^{\text{cca}} (t_1) \cup [t_0 \neq t_k] \mathcal{ST}_{\mathcal{E},k,t_k}^{\text{cca}} (k \ t_0)
\end{align*}
$$

We can then formally express the conditions on
$\phi_{\text{key}}^{\text{k}}(\vec{u}, m, t_r, t_k)$ and $\phi_{\text{rand}}^{\text{r}}(\vec{u}, m, t_r, t_k)$. For every model
$\mathbb{M} : \mathcal{E}$ of $\Theta$, every $\eta \in \mathbb{N}$ and $\rho \in \mathbb{T}_{\mathbb{M},\eta}$, we require that:

1) if $\llbracket \phi_{\text{key}}^{\text{k}}(\vec{u}, m, t_r, t_k) \rrbracket_{\mathbb{M}:\mathcal{E}}^{\eta, \rho} = 1$ then

$$
\llbracket \forall \vec{\alpha}. \psi \Rightarrow t_k \neq t_0 \rrbracket_{\mathbb{M}:\mathcal{E}}^{\eta;\rho} = 1
$$

for every $(\vec{\alpha}, \psi, k t_0) \in \mathcal{ST}_{\mathcal{E},k,t_k}^{\text{euf}}(\vec{u}, m, t_r, t_k)$;

2) if $\llbracket \phi_{\text{rand}}^{\text{k}}(\vec{u}, m, t_r, t_k) \rrbracket_{\mathbb{M}:\mathcal{E}}^{\eta, \rho} = 1$ then

$$
\llbracket \forall \vec{\alpha}. \psi \Rightarrow t_r \neq t_0 \rrbracket_{\mathbb{M}:\mathcal{E}}^{\eta;\rho} = 1
$$

for every $(\vec{\alpha}, \psi, r t_0) \in \mathcal{ST}_{\mathcal{E},k,t_k}^{\text{euf}}(\vec{u}, m, t_r, t_k)$.

In practice, we effectively compute these two formulas in a
way similar to what is explained for the G.EQUIV.FRESH rule
in Appendix F-B.

**Proposition 19.** *The rule G.CCA1 is sound.*

That proposition is proved similarly to the soundness proofs
for the previous two cryptographic rules.

Symmetric case: The rule above applies in the case of
asymmetric encryption. A corresponding rule, though slightly
more complex, can be written in the case of symmetric
encryption.

In that case, the attacker does not get access to the encryption
key, since it is the same as the decryption key. Instead, he
has access to an additional oracle, that encrypts any message,
and can be called any number of times, at any point. This
slightly changes the definition of $\mathcal{ST}_{\mathcal{E},k,t_k}^{\text{cca}}(\cdot)$, to account for this
additional oracle, in the expected way: occurrences of the key as
third argument of the encryption function are not recorded. We
also must add another condition, similar to $\phi_{\text{rand}}^{\text{r}}(\cdot)$, to ensure
that the same random is never used to encrypt two different
plaintexts – indeed, encryptions can only be computed by the
oracle, who samples a fresh random value each time.