I'm a post-doc researcher at INRIA, France, and I'm developing a TLS
implementation (with the goal of formal verification), and I would
like to include support for AEAD ciphers (e.g. AEAD_AES_128_GCM).
However, I got stuck because of the following problem.
According to RFC 5246, sec 6.2.3.3, the additional data (AD) for AEAD
consist of "seq_num + TLSCompressed.type + TLSCompressed.version +
TLSCompressed.length".
Computing such AD, and in particular TLSCompressed.length, is feasible
when encrypting. However, when decrypting it seems impossible to me to
retrieve that value (indeed it should be secret, and the AEAD
ciphertext should not reveal the size of the plaintext, right?
After
all, in the Mac-then-encrypt mode of TLS, random padding is added for
this exact purpose -- and TLSCompressed.length becomes available only
after decryption, and before mac verification).
Can you please explain me where am I wrong?