From what I understand, when using for example AES for encryption and HMAC_SHA256 for MAC generation (and the keys $K_1 \neq K_2$), this means the following:

1. $ciphertext = AES_{K_1}\{plaintext\}$
2. $mac = HMAC\_SHA256_{K_2}\{ciphertext\}$
3. send: $ciphertext \;\|\; mac$

I have two questions regarding this construction:

1. Does it negatively affect security to calculate a hash value of the ciphertext before MAC calculation? Like exchanging step $2.$ with this: $HMAC\_SHA256_{K_2}\{SHA256(ciphertext)\}$.
2. What security properties are offered by this construction in general -- because I don't understand, what about this construction is provably secure.
-
The answers to Should we MAC-then-encrypt or encrypt-then-MAC? discuss the security properties of Encypt-then-MAC and compare them to MAC-then-encrypt and MAC-and-encrypt. –  David Cary Jun 4 '13 at 12:34
@DavidCary That answers the second question, not so much the first one. –  Paŭlo Ebermann Jun 4 '13 at 18:25
Assuming you are not compressing to less than the size of your HMAC (i.e. using SHA1 for the inner hash), it seems it should not affect security. –  Michael Jun 4 '13 at 18:34
I know that HMAC itself is based on twice the application of a hash function, thus you might wonder, why I asked question 1. My reasoning is when I have something like HMAC(some || concatenaed || fields || ciphertext), it might be possible for an attacker to shift the boundary between "fields" and the ciphertext, because ciphertexts usually don't have a fixed length. –  Martin Lundberg Jun 4 '13 at 21:50

Does it negatively affect security to calculate a hash value of the ciphertext before MAC calculation? Like exchanging step 2. with this: HMAC-SHA256(SHA256(ciphertext)).

Technically, yes, but not significantly. In order to attack the scheme you propose, the attacker would have to be able to do at least one of two things: (1) Find an attack on the (standard) HMAC-SHA256 scheme; or (2) Find a collision for SHA256. Currently, the cryptographic community believes that one can safely assume an attacker can do neither of these things. (Contrary to what some may expect, an ability to do the second does not imply an ability to do the first.)

What security properties are offered by this construction in general -- because I don't understand, what about this construction is provably secure.

What do you mean by "this construction"? Do you mean Encrypt-then-Mac, or HMAC-SHA256?

If you meant Encrypt-then-MAC, David Cary provided a link to this question, and you might find the answers helpful. To summarize, one can prove that an attacker cannot learn information about the plaintexts (aside from their lengths), and cannot create a ciphertext that will pass the MAC integrity check. Here, attackers are assumed to have the ability to conduct chosen message attacks; that is, we assume that the attacker can convince or trick one of the parties into sending some messages of the attacker's choosing, and show that having this power is not enough for the attacker to "break" the scheme. (This is very conservative: in the real world, most attackers won't have this ability.) We also assume that the encryption algorithm and the MAC algorithm are themselves secure, and use independently chosen, random keys.

If you meant HMAC-SHA256, then see the second part of my answer to another question. Proving that HMAC-SHA256 has the properties discussed there requires making some (reasonable) assumptions about SHA256.

In both cases, the proofs are not "absolute". We need to make assumptions about the underlying algorithms, and the proof only shows that the probability of the attacker succeeding is very small, provided you don't do something like use the same key to encrypt petabytes of data.

Note: In your question, you wrote Ciphertext = AES_K(Plaintext). But this is (almost always) wrong! AES can only work on 16-byte strings. To encrypt longer strings, you need to use AES inside of some mode of operation.

-
Great answer that is really helpful to me. Thank you. Is there a mode of operation for AES you can recommend? –  Martin Lundberg Jun 4 '13 at 22:36
@MartinLundberg: If you're going to use HMAC for authentication, I'd probably go with AES-CTR or AES-CBC. People seem to love CBC, but I prefer CTR. Alternatively, if you'd like to skip out on the HMAC bit, you can use one of the AEAD modes of operation (like GCM). These provide authentication along with confidentiality, which is really quite nice. –  Reid Jun 5 '13 at 10:03