GCM Implementation and TLSCompressed.Length

[Alfredo Pironti]

Dear list,

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?
I tried to take a quick look at the GnuTLS implementation of GCM (the
only open source TLS implementation I'm aware of implementing GCM),
but I could not find an evident mapping between the AEAD interface
described in RFC 5246 and the code, especially w.r.t. to the AD. Have
you got any hint about it?

Thank you very much in advance for your support.

Best,
Alfredo