On the Soundness of Authenticate-then-Encrypt: Formalizing the Malleability of Symmetric Encryption
Ueli Maurer and Björn Tackmann
A communication channel from an honest sender $A$ to an honest receiver $B$ can be described as a system with three interfaces labeled $A$, $B$, and $E$ (the adversary), respectively, where the security properties of the channel are characterized by the capabilities provided at the $E$-interface.
A security mechanism, such as encryption or a message authentication code (MAC), can be seen as the transformation of a certain type of channel into a stronger type of channel, where the term ``transformation'' refers to a natural simulation-based definition. For example, the main purpose of a MAC can be regarded as transforming an insecure into an authenticated channel, and encryption then corresponds to transforming an authenticated into a fully secure channel; this is the well-known Encrypt-then-Authenticate (EtA) paradigm.
In the dual paradigm, Authenticate-then-Encrypt (AtE), encryption first transforms an insecure into a confidential channel, and a MAC transforms this into a secure channel. As pointed out by Bellare and Namprempre [BN00], and Krawczyk [Kra01], there are encryption schemes for which AtE does not achieve the expected guarantees.
We highlight two reasons for investigating nevertheless AtE as a general paradigm: First, this calls for a definition of confidentiality; what separates a confidential from a secure channel is its (potential) malleability. We propose the first systematic analysis of malleability for symmetric encryption, which, in particular, allows us to state a generic condition on encryption schemes to be sufficient for AtE. Second, AtE is used in practice, for example in TLS. We show that the schemes used in TLS (stream ciphers and CBC encryption) satisfy the condition. This is consistent with Krawczyk's results on similar instantiations of AtE in game-based models.