I'm in search of the correct definition of a stateful authenticated encryption scheme (sAE), and its related security notion. This has been treated several times in the academic literature, however, all the papers I've read contains a discrepancy between how they state the security goal in informal English and their formal security game. In particular, their formal specification of the security game always contains a flaw that allows for a trivial win for the adversary.
Formally, a sAE scheme $\mathcal{SE = (K, E, D)}$ consists of three algorithms, a key generation algorithm $\mathcal{K}$, an encryption algorithm $\mathcal{E}$ which is both randomized and stateful, and a decryption algorithm $\mathcal{D}$, which is deterministic and stateful. The encryption and decryption algorithms are subject to the correctness requirement that if they both start in the initial state, and for $i = 1, 2, \dots,$ if $C_i = \mathcal{E}_K(M_i)$ and $M_i' = \mathcal{D}_K(C_i)$, then it must be that $M_i = M_i'$ for all $i$.
The first paper to formally define a notion of security for sAE was Bellare et al in Authenticated Encryption in SSH: Provably Fixing the SSH Binary Packet Protocol. They define the interaction between the encryptor and decryptor to be in-sync, if at any point in time, the sequence of inputs to the decryptor is a prefix of the outputs of the encryptor. They are out-of-sync if they are not in-sync. This is their informal statement of the security game capturing stateful privacy IND-SFCCA (note that this paper splits the security of an sAE scheme into an individual security requirements for privacy and one for integrity, whereas later papers merge these into one combined game. The game formulations are still very similar, and are also equivalent in terms of security: Appendix B):
And this is their formal definition (Appendix A. Def. A.2):
The flaw: In the formal definition, the $\mathcal{D}_K$ oracle returns something other than $\perp$ if: (1) $j > i$ i.e., $C$ is a proper out-of-sync message or (2) $C \neq C_v$, i.e., the submitted ciphertext was not the latest ciphertext output from the encryptor. Notice a flaw with this?
Assume the attacker first asks his $\mathcal{E}_K$ oracle for some messages $M_1, M_2, M_3$, say, and are given back $C_1, C_2, C_3$. He then calls $\mathcal{D}_K$ on $C_2$. Notice that $i = 3$ and $j = 1$, so (1) is not true, but (2) is, since $C_2 \neq C_1$. Hence we enter $\mathsf{phase} = 1$, and the adversary receives the decryption of $C_2$ and can trivially win the game.
Now you might simply dismiss this as a trivial "typo"/oversight, and that the authors really meant to write something equivalent to their informal description. However, this security definition, with the same flaw, has been repeated in several other papers by different authors:
- On the security of TLS-DHE in the standard model (Def.5, Fig. 1 and Fig. 4)
- On the security of TLS-DH and TLS-RSA in the standard model (Def.7 and Fig.1)
- On the security of the TLS protocol: a systematic analysis (Appendix B.1, and Fig. 6)
In addition, you have the paper by Brzuska et al Less is More: Relaxed yet Composable Security Notions for Key Exchange, who provides a summary of the above definition (Def.16, p. 29) in their own (and different) framework, recreating the same flawed behavior!
So what's going on here?
