Cryptanalysis of GlobalPlatform Secure Channel Protocols

Abstract

GlobalPlatform (GP) card specifications are the de facto standards for the industry of smart cards. Being highly sensitive, GP specifications were defined regarding stringent security requirements. In this paper, we analyze the cryptographic core of these requirements; i.e. the family of Secure Channel Protocols (SCP). Our main results are twofold. First, we demonstrate a theoretical attack against SCP02, which is the most popular protocol in the SCP family. We discuss the scope of our attack by presenting an actual scenario in which a malicious entity can exploit it in order to recover encrypted messages. Second, we investigate the security of SCP03 that was introduced as an amendment in 2009. We find that it provably satisfies strong notions of security. Of particular interest, we prove that SCP03 withstands algorithm substitution attacks (ASAs) defined by Bellare et al. that may lead to secret mass surveillance. Our findings highlight the great value of the paradigm of provable security for standards and certification, since unlike extensive evaluation, it formally guarantees the absence of security flaws.

Appendices

A Proof of Proposition 1

We start by providing three definitions that we will use throughout our proof.

MAC Function. Here, we just recall how a MAC scheme is related to its MAC function. Let $\mathcal {MA}[F] = (\mathcal {K},\mathcal {T},\mathcal {V})$ be a MAC scheme based on the MAC function F. F takes as input a key $\mathsf {K}$ and a message M to output a tag $\tau$. The tagging algorithm $\mathcal {T}_{\mathsf {k}}$ and the verification algorithm $\mathcal {V}_{\mathsf {k}}$ are defined as follows:

Truncated MAC. Let $T: \{0,1\}^{n} \longrightarrow \{0,1\}^{n_{T}}$ be a transformation function. Let $\mathcal {MA}[F] = (\mathcal {K},\mathcal {T},\mathcal {V})$ be a MAC scheme based on the MAC function F. We define the transformed MAC scheme $T o \mathcal {MA} = (\mathcal {K},T o \mathcal {T},T o \mathcal {V})$ that uses ToF as its MAC function, where o denotes the composition operator. A truncated MAC is a transformed MAC in which T(.) is the $\texttt {MSB}_{l}(.)$ function that takes a message as input and returns the l most significant (i.e. left-most) bits.

Tweak Chaining MAC2 ( $\mathcal {TC}\text {-}\widetilde{\mathcal {MA}}2$ ). Let $\widetilde{F}_{\mathsf {k}}: \{0,1\}^{n} \times \texttt {MSG} \longrightarrow \{0,1\}^{n}$ be a tweakable function and let $\mathcal {TC}\text {-}\widetilde{\mathcal {MA}}$ be its associated chaining scheme. We define $\mathcal {TC}\text {-}\widetilde{\mathcal {MA}}2$ as $\mathcal {TC}\text {-}\widetilde{\mathcal {MA}}$ except that $\mathcal {TC}\text {-}\widetilde{\mathcal {MA}}2$ operates on the entire tag returned by $\widetilde{F}(.,.)$ and not only on its half as in $\mathcal {TC}\text {-}\widetilde{\mathcal {MA}}$. Stated differently, $\mathcal {TC}\text {-}\widetilde{\mathcal {MA}}2$ is a MAC scheme in which the MAC function F2 is defined as follows:

where chained is a static variable (i.e. maintains its value between calls) that was initialized with $\mathbf {0}^{n}$.

Having thus presented the above definitions, we are now on a position to make our proof. Let $\widetilde{F}_{\mathsf {k}}: \{0,1\}^{n} \times \texttt {MSG} \longrightarrow \{0,1\}^{n}$ be a tweakable function and let $\mathcal {TC}\text {-}\widetilde{\mathcal {MA}}2[F2]$ be its associated tweak chaining MAC2 scheme. We notice that the $\mathcal {TC}\text {-}\widetilde{\mathcal {MA}} = (\widetilde{\mathcal {K}},\widetilde{\mathcal {T}},\widetilde{\mathcal {V}})$ scheme presented in Definition 7 can be seen as the truncated MAC of $\mathcal {TC}\text {-}\widetilde{\mathcal {MA}}2[F2]$, where $T(.) = \texttt {MSB}_{n/2}(.)$. Thus, we denote the MAC function of $\mathcal {TC}\text {-}\widetilde{\mathcal {MA}}$ as ToF2.

Consider any polynomial-time SUF-CMA adversary $\mathbf {A}$ against $\mathcal {TC}\text {-}\widetilde{\mathcal {MA}}$. Recall that $\mathbf {A}$ can make two types of queries: tagging queries and verification queries. We suppose that $\mathbf {A}$ makes q tagging queries. We associate two adversaries to $\mathbf {A}$: an sPRF adversary $\mathbf {B}$ against the MAC function F2 (or equivalently against $\mathcal {TC}\text {-}\widetilde{\mathcal {MA}}2[F2]$), and an $\widetilde{\text {IND}}$-CPA distinguisher $\mathbf {D}$ against the tweakable function $\widetilde{F}_{\mathsf {k}}$. Now, we state the following lemmas in which we define how the adversaries $\mathbf {A}$, $\mathbf {B}$ and $\mathbf {D}$ interact between each other and from which the Proposition 1 follows directly.

Lemma A.1

$\mathbf {Adv}_{\mathcal {TC}\text {-}\widetilde{\mathcal {MA}}}^{\textit{suf-cma}}(A) = \mathbf {Adv}_{F2}^{\textit{sprf}}(B) + 1/2^{n/2}$

Lemma A.2

$\mathbf {Adv}_{F2}^{\textit{sprf}}(B) \le \mathbf {Adv}_{\widetilde{F}}^{\widetilde{\textit{ind}}{} \textit{-cpa}}(D) + \mathsf {Pr[Col]} + \mathsf {Pr[Col_{q}]}$

Lemma A.3

$\mathsf {Pr[Col]} \le q^{2}/2^{n}$

Proof of Lemma A.1 : Recall that $\mathbf {B}$ has access to the oracle $\mathcal {O}$ and her goal is to distinguish whether $\mathcal {O}$ is the MAC function F2 or the stateful random oracle $\mathcal {R}_{\mathcal {S}}$. Recall also that the MAC function of $\mathcal {TC}\text {-}\widetilde{\mathcal {MA}}$ is ToF2. The algorithm $\mathbf {B}$ is described below:

We can see that $\mathbf {B}$ perfectly simulates the answers to $\mathbf {A}$. In addition, $\mathbf {B}$ returns 1 (i.e. guesses that the oracle $\mathcal {O}$ is the MAC function F2) when $\mathbf {A}$ succeeds in forging a tag. Therefore, the following relation holds:

$$\begin{aligned} \mathsf {Pr}[\mathbf {A}^{T o \mathcal {O}} \text { forges}] = \mathsf {Pr}[\mathbf {B}^{\mathcal {O}} \Rightarrow 1] \end{aligned}$$

(1)

where we use the equivalent notation in which we note that the adversary $\mathbf {A}$ has access to the MAC function as oracle instead of the tagging/verification oracles.

By definition of strong unforgeability of the MAC scheme $\mathcal {TC}\text {-}\widetilde{\mathcal {MA}}$ (see Definition 2), the advantage of $\mathbf {A}$ is defined by the probability of her success when she has access to the oracle ToF2. Therefore, we have:

$$\begin{aligned} \mathbf{Adv }_{\mathcal {TC}\text {-}\widetilde{\mathcal {MA}}}^{\textit{suf-cma}}(\mathbf {A})&= \mathsf {Pr}[\mathbf {A}^{T o F2} \text { forges}] \\&= \mathsf {Pr}[\mathbf {A}^{T o F2} \text { forges}] + \left( \mathsf {Pr}[\mathbf {A}^{T o \mathcal {R}_{\mathcal {S}}} \text { forges}] - \mathsf {Pr}[\mathbf {A}^{T o \mathcal {R}_{\mathcal {S}}} \text { forges}]\right) \\&= \left( \mathsf {Pr}[\mathbf {A}^{T o F2} \text { forges}] - \mathsf {Pr}[\mathbf {A}^{T o \mathcal {R}_{\mathcal {S}}} \text { forges}]\right) + \mathsf {Pr}[\mathbf {A}^{T o \mathcal {R}_{\mathcal {S}}} \text { forges}] \\&= \left( \mathsf {Pr}[\mathbf {B}^{F2} \Rightarrow 1] - \mathsf {Pr}[\mathbf {B}^{\mathcal {R}_{\mathcal {S}}} \Rightarrow 1]\right) + \mathsf {Pr}[\mathbf {A}^{T o \mathcal {R}_{\mathcal {S}}} \text { forges}] \ \text {(from 1)} \\&= \mathbf{Adv }_{F2}^{\textit{sprf}}(B) + \mathsf {Pr}[\mathbf {A}^{T o \mathcal {R}_{\mathcal {S}}} \text { forges}] \end{aligned}$$

Now, we examine $\mathsf {Pr}[\mathbf {A}^{T o \mathcal {R}_{\mathcal {S}}} \text { forges}]$, which is equal to the probability that $\mathbf {A}$ forges against a MAC scheme that has $T o \mathcal {R}_{\mathcal {S}}$ as its MAC function. Recall that $\mathcal {R}_{\mathcal {S}}$ is a random oracle. Let us suppose that $(M,\tau )$ is the forging query that $\mathbf {A}$ uses to break the scheme. Therefore, the following relations holds: $\tau = T\left( \mathcal {R}_{\mathcal {S}}(M)\right)$. Thus, we conclude our proof by showing that we have:

$$\begin{aligned} \mathsf {Pr}[\mathbf {A}^{T o \mathcal {R}_{\mathcal {S}}} \text { forges}]&= \mathsf {Pr}[x \mathop {\longleftarrow }\limits ^{R} \{0,1\}^{n},\ T(x) = \tau ] \\&= \frac{1}{2^{n/2}} \qquad \left( \text {since } T(.) = \texttt {MSB}_{n/2}(.)\right) \end{aligned}$$

Proof of Lemma A.2 : Here, we consider any sPRF adversary $\mathbf {B}$ against F2 and we associate it to a particular $\widetilde{\text {IND}}$-CPA distinguisher $\mathbf {D}$ against the tweakable function $\widetilde{F}_{\mathsf {k}}: \{0,1\}^{n} \times \texttt {MSG} \longrightarrow \{0,1\}^{n}$. Recall that $\mathbf {D}$ has access to the oracle $\mathcal {O}(.,.)$ and her goal is to distinguish whether $\mathcal {O}$ is $\widetilde{F}_{\mathsf {k}}(.,.)$ or $\widetilde{\mathcal {R}}(.,.)$, where $\widetilde{\mathcal {R}}(.,.)$ is a function that, on input (T, M), returns n-bit random strings. Recall also that $\mathbf {D}$ is a tweak-respecting adversary (i.e. does not repeat tweak). We define the algorithm of $\mathbf {D}$ as follows:

where $\mathsf {S}$ is a multiset in which values can repeat. We argue that when $\mathsf {S}$ does not contain the same value twice, $\mathbf {D}$ is perfectly simulating $\mathbf {B}$’s execution environment. This is true because $\widetilde{F}(.,.)$ is no distinguishable from the random oracle $\widetilde{\mathcal {R}}(.,.)$ only against tweak-respecting adversaries. We illustrate the importance of such a condition by an example. In our example, we take $\widetilde{\text {OMAC}}(T,M)\ (= \text {OMAC}(T||M))$ as the tweakable function $\widetilde{F}(.,.)$. Now, we show that $\mathbf {B}$ can easily see under the simulation environment that she is not interacting with a random oracle. $\mathbf {B}$ knows that the initial tweak (i.e. state) is $\mathbf {0}^{n}$ and queries $M_{1} = \mathbf {0}^{n}$ to receive $\tau _{1}$ from her oracle. Then, let T be a tweak that repeats twice. For the first occurrence of T, $\mathbf {B}$ queries $M_{2} = \mathbf {0}^{n}$ to receive $\tau _{2}$ and for its second occurrence she queries $M_{2} = \mathbf {0}^{n}\,||\,\tau _{2}\,||\,\mathbf {0}^{n}$ to receive $\tau _{3}$. It is easy to see that $\tau _{1} = \tau _{3}$ when $\mathcal {O} = \widetilde{F}_{\mathsf {k}}(.,.)\ ({\ne }\widetilde{\mathcal {R}}(.,.))$. Indeed, we have

Thus, from $\mathbf {D}$’s algorithm, we can see that

$$\begin{aligned} \mathsf {Pr}[\mathbf {D^{\widetilde{F}}} \Rightarrow 1]&= \mathsf {Pr}[\mathbf {B}^{F2} \Rightarrow 1] \,+ \mathsf {Pr}[\mathsf {S}|\widetilde{F}] \\ \mathsf {Pr}[\mathbf {D^{\widetilde{\mathcal {R}}}} \Rightarrow 1]&= \mathsf {Pr}[\mathbf {B}^{\mathcal {R}_{\mathcal {S}}} \Rightarrow 1] + \mathsf {Pr}[\mathsf {S}|\widetilde{\mathcal {R}}] \end{aligned}$$

where $\mathsf {Pr[S]}$ is the probability that the multiset $\mathsf {S}$ contains duplicate values.

By using the two above relations, we get

$$\begin{aligned} \mathbf{Adv }_{F2}^{\textit{sprf}}(B)&= \mathbf{Adv }_{\widetilde{F}}^{\widetilde{\textit{ind}}{} \textit{-cpa}}(D) + \overbrace{\mathsf {Pr}[\mathsf {S}|\mathcal {R}]}^{\mathsf {Pr[Col]}} -\; \overbrace{\mathsf {Pr}[\mathsf {S}|\widetilde{F}]}^{\mathsf {Pr[Col_{q}]}} \\&\le \mathbf{Adv }_{\widetilde{F}}^{\widetilde{\textit{ind}}{} \textit{-cpa}}(D) + \mathsf {Pr[Col]} + \mathsf {Pr[Col_{q}]} \end{aligned}$$

where $\mathsf {Pr[Col_{q}]}$ is the collision probability of the tweakable function $\widetilde{F}$ after q messages. Thus, our proof ends.

Proof of Lemma A.3 : Informally speaking, the lemma means that the set $\{x: x_{0} = \mathbf {0}^{n},\ x_{i} = \mathcal {R}(x_{0},.)\}$ has asymptotically negligible probability to include duplicate values. Recall that q is the number of $\mathbf {B}$’s queries. We start our proof by making induction on q. For all $q \ge 1$, we prove that

$$\begin{aligned} \mathsf {Pr[Col]} = \frac{q(q+1)}{2^{n+1}} \end{aligned}$$

(2)

Then, we conclude our proof by noticing that $q(q+1)/2^{n+1} \le q^{2}/2^{n}$.

Base case. When $q = 1$, the right side of (2) is $1/2^{n}$. Now, let’s look at the left side. After only one call, there are two elements in $\mathsf {S}$: $\left\{ \mathbf {0}^{n}, y\right\}$, where $y \longleftarrow \mathcal {R}(\mathbf {0}^{n}, .)$. Thus, $\mathsf {Pr[Col]} = \mathsf {Pr}[x \mathop {\leftarrow }\limits ^{R} \{0,1\}^{n}, x = \mathbf {0}^{n}]$, which is equal to $1/2^{n}$.

Induction step. Suppose that the Eq. 2 is true for $q = m - 1$. Here, $x_{i}$ denotes the ith element of the multiset $\mathsf {S}$. After $q = m$ calls, we have

$$\begin{aligned} \mathsf {Pr[Col]}&= \overbrace{\mathsf {Pr[Col \text { after } m-1 \text { calls}]}}^{\text {induction hypothesis}} + \mathsf {Pr}[x_{m} \in \mathsf {S}] \\&= \frac{m(m-1)}{2^{n+1}} + \frac{m}{2^{n}} \\&= \frac{m(m+1)}{2^{n+1}} \end{aligned}$$

Hence, the Eq. 2 holds for $q=m$, and the induction step is complete.

B Proof of Theorem 1

Recall that $\mathbf {A}$ can make two types of queries: encryption queries and decryption queries. We denote $\mathbf {A}$’s i-th encryption query as $M_{i}$ and the returned ciphertext as $C_{i} = \sigma _{i}||\tau _{i}$. We denote $\mathbf {A}$’s i-th decryption query as $C'_{i} = \sigma '_{i}||\tau '_{i}$ and the returned message as $m_{i}$. We associate to $\mathbf {A}$ an SUF-CMA forger $\mathbf {F}$ against $\mathcal {TC}$-$\widetilde{\mathcal {MA}}$. This association is similar to the one given in the Case 1 of Theorem 4: $\mathbf {F}$ generates a key $\mathsf {K1}\in \texttt {Key}$ that she uses for the encryption/decryption algorithms of Sf-n$\mathcal {SE}$. We recall that the forger $\mathbf {F}$ has access to two oracles: a tagging oracle $\widetilde{\mathcal {T}}_{\mathsf {k2}}$ and a verification oracle $\widetilde{\mathcal {V}}_{\mathsf {k2}}$, where the key $\mathsf {K2}$ is independent from $\mathsf {K1}$. Below, we describe our trivial association.

• 1. When $\mathbf {A}$ makes an encryption query M, $\mathbf {F}$ outputs $\sigma \longleftarrow \mathsf {Enc}\left( n\mathcal {E}_{\mathsf {k1}}\text {-Sf}(M)\right)$. Then, she queries $\sigma$ to her tagging oracle $\widetilde{\mathcal {T}}_{\mathsf {k2}}$ and receives $\tau$ in response. Finally, she outputs $C = \sigma \,||\,\tau$ to $\mathbf {A}$.

• 2. When $\mathbf {A}$ makes a decryption query $C = \sigma \,||\,\tau$, the forger $\mathbf {F}$ queries $\tau$ to her verification oracle $\widetilde{\mathcal {V}}_{\mathsf {k2}}$ and receives a binary value b. If b is false, then $\mathbf {F}$ halts after outputting $\bot$. Otherwise, $\mathbf {F}$ computes $n\mathcal {D}_{\mathsf {k1}}\text {-Sf}\left( \mathsf {Dec}(\sigma )\right)$ and outputs the result to $\mathbf {A}$.

• 3. When $\mathbf {A}$ wins in her INT-SFCTXT experiment, namely providing a new valid out-of-sync decryption query $C = \sigma \,||\,\tau$, then $\mathbf {F}$ stops and attempts to evaluate the pair $(\sigma ,\tau )$ in order to see whether she succeeds in her forgery. The different cases are presented below in the proof of Lemma B.1.

Now, suppose $\mathbf {A}$ has made q encryption queries and d decryption ones. Let j be the index of $\mathbf {A}$’s first out-of-sync decryption query. We only consider the first out-of-sync query because if it fails, the decryption algorithm will return $\bot$ and halt for all ensuing queries (see our discussion about the approach of halting state in Sect. 4.1). We define two events in case the $\mathbf {A}$’s j-th decryption query succeeds: (1) $\mathsf {Col}$: $\exists i \le q$ such that $\tau '_{j} = \tau _{i}$ and $i \ne j$; (2) $\mathsf {Bad}$: $q \ge j$, $\tau '_{j} = \tau _{j}$ and $m_{j} = M_{j}$. We state the following lemmas from which Theorem 1 follows directly (using Proposition 1).

Lemma B.1

$\mathbf {Adv}_{\text {Sf-nEtTw}}^{\text {int-sfctxt}}(A) \le \mathbf {Adv}_{\mathcal {TC}\text {-}\widetilde{\mathcal {MA}}}^{\text {suf-cma}}(F) + \mathsf {Pr[q\text {-}Col]} + \mathsf {Pr[Bad]}$

Lemma B.2

$\mathsf {Pr[Bad]} = 0$

Proof of Lemma B.1 : As said previously, $\mathbf {A}$ made q encryption queries before her first out-of-sync query ($\mathcal {Q}$) which is the j-th decryption query $(C'_{j} = \sigma '_{j}\,||\,\tau '_{j})$. We define the following events.

If $\mathcal {Q}$ fails, then $\mathbf {A}$ cannot win any more, since the decryption algorithm will return $\bot$ for any subsequent query. Therefore, $\mathbf {Adv}_{\text {Sf-nEtTw}}^{\textit{int-sfctxt}}(A) = \mathsf {Pr}[E]$. Considering the different events, we have $\mathsf {Pr}[E] = \mathsf {Pr}[E_{1} \vee E_{2,2,2}] + \mathsf {Pr}[E_{2,1}] + \mathsf {Pr}[E_{2,2,1}]$.

Now, we study the probabilities of these events. We can see that $E_{2,1}$ corresponds to the event $\mathsf {Col}$, since it implies that $\tau '_{j}$ has already been produced before and that was not during the j-th encryption query (this includes the fact that $\mathbf {A}$ might not have made j encryption queries yet). Concerning $E_{2,2,1}$, it is easy to see that it satisfies the definition of the $\mathsf {Bad}$ event. Consequently, we have

$$ \mathbf {Adv}_{\text {Sf-nEtTw}}^{\textit{int-sfctxt}}(A) = \mathsf {Pr}[E_{1} \vee E_{2,2,2}] + \mathsf {Pr[Col]} + \mathsf {Pr[Bad]} $$

We conclude the proof by examining $\mathsf {Pr}[E_{1} \vee E_{2,2,2}]$ and $\mathsf {Pr[Col]}$.

$\pmb {\mathsf {Pr}[E_{1} \vee E_{2,2,2}]}$. We notice that when the event $E_{1} \vee E_{2,2,2}$ occurs, (i.e. the j-th decryption oracle $C'_{j} = \sigma '_{j}\,||\,\tau '_{j}$ does not return $\bot$), then the forger $\mathbf {F}$ succeeds in finding an SUF-CMA forgery against $\mathcal {TC}$-$\widetilde{\mathcal {MA}}$, since the two events ensure that the pair $(m_{j},\tau '_{j})$ was never produced before by the oracle $\widetilde{\mathcal {T}}_{\mathsf {k2}}$.

Indeed, the event $E_{1}$ implies that $\tau '_{j}$ has never been queried to $\widetilde{\mathcal {T}}_{\mathsf {k2}}$, while the event $E_{2,2,2}$ implies that the tag $\tau '_{j}$ has never been obtained from querying the oracle $\widetilde{\mathcal {T}}_{\mathsf {k2}}$ with $\sigma '_{j}$ as input. This is because for any state i, the following implication is asymptotically true (i.e. n$\mathcal {E}_{\mathsf {k}}\text {-Sf}(.)$ is injective):

$$ M_{i} \ne M'_{i} \Longrightarrow n\mathcal {E}_{\mathsf {k1}}\text {-Sf}(M_{i}) \ne n\mathcal {E}_{\mathsf {k1}}\text {-Sf}(M'_{i}) $$

Therefore, $\tau '_{j}$ $(= \tau _{j})$ was computed for $\sigma _{j} = n\mathcal {E}_{\mathsf {k1}}\text {-Sf}(M_{j})$ which is different from $\sigma '_{j}$ (i.e. $\sigma _{j} \ne \sigma '_{j})$, since $\sigma '_{j} = n\mathcal {E}_{\mathsf {k1}}\text {-Sf}(m_{j})$ and $M_{j} \ne m_{j}$.

Thus, we have

$$ \mathsf {Pr}[E_{1} \vee E_{2,2,2}] = \mathsf {Pr}[\mathbf {F} forges] = \mathbf {Adv}_{\mathcal {TC}\text {-}\widetilde{\mathcal {MA}}}^{\textit{suf-cma}}(F) $$

$\pmb {\mathsf {Pr[Col]}}$. As previously pointed out, $\mathsf {Pr[Col]} = \mathsf {Pr}[\exists i \ne j \text { such that } \tau '_{j} = \tau _{i}]$. This means that for two different states the following equality holds:

$$ \widetilde{\mathcal {T}}_{\mathsf {k}2}(\mathsf {Enc}(n\mathcal {E}_{\mathsf {k1}}\text {-Sf}(m_{j}))) = \widetilde{\mathcal {T}}_{\mathsf {k}2}(\mathsf {Enc}(n\mathcal {E}_{\mathsf {k1}}\text {-Sf}(M_{i}))) $$

The above relation supposes that the adversary should find a collision against $\mathcal {TC}$-$\widetilde{\mathcal {MA}}$ after q invocations to the $\widetilde{\mathcal {T}}_{\mathsf {k2}}(.)$ oracle, which corresponds to find a state $i (\ne j)$ such that the related MAC tag is equal to the one computed for the state j. By looking at the construction of $\mathcal {TC}\text {-}\widetilde{\mathcal {MA}}$ in Definition 7, we find that $\mathsf {Pr[Col]}$ is equivalent to the probability of encountering a collision against the underlying tweakable function $\widetilde{F}_{\mathsf {k2}}(.,.)$. Stated differently, we have

$$ \mathsf {Pr[Col]} = \mathsf {Pr[q\text {-}Col]} $$

where, we recall that, given a message M and a list $\mathsf {S}$ containing q outputs of $\widetilde{F}_{\mathsf {k}2}$, $\mathsf {Pr[q\text {-}Col]}$ is the probability that $\widetilde{F}_{\mathsf {k2}}(M) \in \mathsf {S}$.

Proof of Lemma B.2 : The event $E_{2,2,1}$ includes all the following events: (1) $q \ge j$; (2) the decryption query $C'_{j} = \sigma '_{j}||\tau '_{j}$ is out-of-sync, hence $C_{j} \ne C'_{j}$; (3) $\sigma '_{j} \ne \sigma _{j}$, since $\tau '_{j} = \tau _{j}$; and (4) $m_{j} = M_{j}$. We notice that the events 3 and 4 are contradictory, and therefore $\mathsf {Pr[Bad]} = 0$. Indeed, recall that $n\mathcal {SE} = (\mathcal {K}, n\mathcal {E}, n\mathcal {D})$ encrypts messages using a deterministic algorithm. Therefore, for a fixed nonce N, $n\mathcal {E}_{\mathsf {k1}}(N, M_{1}) \ne n\mathcal {E}_{\mathsf {k1}}(N, M_{2})$ implies that $M_{1} \ne M_{2}$. Also, we notice that the encryption and the decryption states were in-sync prior to the j-th decryption query. This means that the associated Sf-n$\mathcal {SE} = (\mathcal {K}\text {-Sf}, n\mathcal {E}\text {-Sf}, n\mathcal {D}\text {-Sf})$ has called $n\mathcal {SE}$ algorithms with the same nonce for each state. Thus, the event 3 entails $\sigma '_{j} = n\mathcal {E}_{\mathsf {k1}}\text {-Sf}(m_{j}) \ne n\mathcal {E}_{\mathsf {k1}}\text {-Sf}(M_{j}) = \sigma _{j}$, which implies $m_{j} \ne M_{j}$. This concludes our proof, since the event 4 is $m_{j} = M_{j}$.

C Collision Probabilities

1.1 C.1 OMAC Collision Probabilities

Here, we state two Results proved in [28] about collisions in OMAC.

Result C.1

[$\mathsf {Pr[Col]_{2}}$]. Let $E_{\mathsf {k}}$ be a block cipher of size l and let $\text {OMAC}[E_{\mathsf {k}}]$ be its associated OMAC scheme. For the sake of simplicity, we only consider messages M whose length is a multiple of l (i.e. |M| / l is an integer). Given a message M, we denote by $\mu$ the number of its blocks, namely $\mu = |M|/l$. Consider two messages M and $M'$, then the following relation characterizes the probability of the OMAC collision:

$$ \Pr [\mathsf {Col}_{2}] = \Pr [\mathsf {Col}(M,M')] \le \frac{(\mu + \mu ')^{2}}{2^{l}} $$

Result C.2

[$\mathsf {Pr[Col]_{q}}$]. Let $E_{\mathsf {k}}$ be a block cipher of size l and let $\text {OMAC}[E_{\mathsf {k}}]$ be its associated OMAC scheme. For the sake of simplicity, we only consider messages M whose length is a multiple of l (i.e. |M| / l is an integer). Given a message M, we denote by $\mu$ the number of its blocks, namely $\mu = |M|/l$. Given a list $\mathcal {Q}$ of q messages, the following relation characterizes the probability of the OMAC collision on $\mathcal {Q}$:

$$ \Pr [\mathsf {Col}_{q}] = \Pr [\mathsf {Col}(\mathcal {Q})] \le \frac{\left( \sum _{i=1}^{q}\mu _{i}\right) ^{2}}{2^{l}} $$

1.2 C.2 Proof of Lemma 5.1

We need to compute both $\mathsf {Pr[Col_{q}]}$ and $\mathsf {Pr[q\text {-}Col]}$. The case of $\mathsf {Pr[Col_{q}]}$ is easy and it can be immediately obtained from Result C.2. Concerning the case $\mathsf {Pr[q\text {-}Col]}$, it can be calculated from Result C.1. Indeed, given a message M and a list $\mathsf {S}$, $\mathsf {Pr[Col_{q}]}$ can be expressed as the sum of the collision probabilities $\mathsf {Pr[Col_{2}^{i}]}$ between M and a message $M_{i}$ for all $M_{i} \in \mathsf {S}$. Here, $M_{\text {max}}$ denotes any message of maximum length and $\mu _{\text {max}}$ denotes its number of blocks. Therefore, we have

$$ \mathsf {Pr[q\text {-}Col]} \le \sum _{i=1}^{q}\mathsf {Pr}[\mathsf {Col}(m_{\text {max}},m_{i})] \le \sum _{i=1}^{q}\frac{(\mu _{\text {max}} + \mu _{i})^{2}}{2^{n}} $$

From all the relations above, we have

$$\begin{aligned} \epsilon&= \frac{q^2}{2^{n}} + \frac{1}{2^{n/2}} + \mathsf {Pr[Col_{q}]} + \mathsf {Pr[q\text {-}Col]} \\&\le \frac{1}{2^{n/2}} + \frac{q^{2}}{2^{n}} + \frac{\left( \sum _{i=1}^{q}\mu _{i}\right) ^{2}}{2^{n}} + \frac{\sum _{i=1}^{q}(\mu _{\text {max}} + \mu _{i})^{2}}{2^{n}} \\&\le \frac{1}{2^{n/2}} + \frac{q^{2}}{2^{n}} + \frac{\left( \sum _{i=1}^{q}\mu _{i}\right) ^{2}}{2^{n}} + \frac{3q\mu _{\text {max}}^{2} + \sum _{i=1}^{q}\mu _{i}^{2}}{2^{n}} \\&\le \frac{1}{2^{n/2}} + \frac{q\left( q + (2\mu _{\text {max}})^{2}\right) + \left( \sum _{i=1}^{q}\mu _{i}\right) ^{2} + \sum _{i=1}^{q}\mu _{i}^{2}}{2^{n}} \end{aligned}$$

which is asymptotically negligible.