On Fri, 6 Dec 2024, 10:06 Muhammad Usama Sardar, < muhammad_usama.sar...@tu-dresden.de> 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) >
_______________________________________________ TLS mailing list -- tls@ietf.org To unsubscribe send an email to tls-le...@ietf.org
