[TLS] Re: Adoption call for RFC 9147bis

[Ben Smyth <[e-mail]>]

On Fri, 6 Dec 2024, 10:06 Muhammad Usama Sardar, <
[e-mail]> wrote:

> On 05.12.24 11:03, Ben Smyth wrote:
>
> If they aren't in the model, then analysis is only good up to KeyUpdate.
>
> Sure, I completely agree. We have no guarantees on what is not in the
> formal model. More precisely, I would like the FATT to comment on the
> following:
>
> Since issues have already been found by David, does FATT expect more
> potential issues around KeyUpdate and post-handshake messages that have
> *not* yet been found? If yes:
>
>    - (at least) one example of such potential issue.
>
>
Post-handshake client authentication is one aspect that could be
investigated. Another could be security under a new key. It's plausible
flaws may exist, we just don't believe there are; any issues would be more
likely to arise in corner cases.

>
>    - What kind of tools are most suitable for such an analysis? I suspect
>    a standard model checker (e.g., SPIN) would do (in contrast to symbolic
>    security analysis tools, like ProVerif and Tamarin).
>
> Unsure standard model checkers would help, symbolic security tools seem
the most useful, plus they only require extension of existing models.

> (OpenJDK got KeyUpdate wrong, there were use cases with no security.)
>
> Sounds interesting. Do you have a pointer for me which describes the
> problem precisely?
>

OpenJDK's TLS 1.3 implementation was vulnerable to attack for large data
volumes after closure in one direction:

* Method tryKeyUpdate() "Do[es]n't bother to kickstart if...the connection
is not duplex-open."

Safe AES-GCM operation is upper-bound by about 395 gigabytes of plaintext
under the same key, thereafter OpenJDK was vulnerable to attack, it's been
patched:
https://github.com/openjdk/jdk/commit/14aad787a81368ced426c2a9cb301f4ff0c37c3f

(The official report doesn't reveal much:
https://www.cve.org/CVERecord?id=CVE-2023-21930)

>