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. * 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).
Sounds interesting. Do you have a pointer for me which describes the problem precisely?(OpenJDK got KeyUpdate wrong, there were use cases with no security.)
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ TLS mailing list -- tls@ietf.org To unsubscribe send an email to tls-le...@ietf.org
