Hi John, Thank you for sharing your insights.
I definitely do not claim that formal analysis is the only thing that should be done. My position is that it is the combination of simulation, cryptanalysis, symbolic security analysis, computational analysis, etc. that makes protocol robust and I believe we have all in this WG, which makes it the strongest one in the IETF. Formal analysis is just one part in it but an important one.
I'll briefly mention why I think it is important. My experience is that many protocol designs (for example attested TLS) I thought should be secure intuitively were actually shown to be insecure by ProVerif, and so over the years I have developed more trust in ProVerif.
I've tried to address your comments in this PR [0], and would welcome any further comments, if you believe it is not addressing your comments.
On 03.03.26 13:13, John Mattsson wrote:
Good with a discussion on formal analysis.>explicitly indicate on a very prominent place, preferably abstract, whether the draft has gone through FATT review or not,I think formal analysis should be treated like any other form of analysis and referenced where appropriate, for example in the Security Considerations section.
Sure, I agree, that Security Considerations section seems like the right place to reference the formal analysis.
However, the point I was making here was a little bit different, namely to distinguish intuition/guesswork from actual FATT review. For example, I'll feel better if ML-KEM draft had a statement like:
This document did not go through the TLS FATT review process.I've removed "very prominent place, preferably abstract" and tried to clarify this point in the editor's draft.
While I think it is excellent that the IETF is using formal analysis as a tool, I am seeing a tendency toward placing too much faith in it. Like all security proofs, formal analysis is only as strong as its assumptions and model. The scope is typically limited, and the model does not necessarily capture real-world deployment complexity, implementation details, operational constraints, or misuse scenarios.
I can attest to that, and to be clear, I don't intend to overclaim. I've added these limitations in the editor's draft.
The public formal verification effort around RFC 8446 was highly valuable and resulted in a number of publicly accessible papers and improved understanding of the protocol. However, my impression is that the experience with the current FATT process has been more mixed.
I suspect that is because for simpler extensions, the delta between human intuition and formal results is smaller. My view is that if the extension of TLS is complex enough (e.g., key update), formal analysis offers valuable insights in terms of:
1. vulnerability finding 2. exposing hidden assumptions by bringing them explicitly in the propertiesI welcome you to check out attested TLS work, for example. My experience is that formal analysis has added a lot of value there in finding corner cases, and the novel attacks we have found [1] by formal analysis have been publicly acknowledged by the systems community (see [2] for example). They denied the attacks we showed them from our formal analysis for quite some time until last week.
Thank you for helping to improve the document and I'll happily address any further comments or concerns that you may have.
Best regards, -Usama[0] https://github.com/muhammad-usama-sardar/tls-fatt-extension/pull/4/changes
[1] https://mailarchive.ietf.org/arch/msg/tls/8lyqHh9y7_Lv6b1iXhpUqYrp0M0/[2] https://web.archive.org/web/20260227160554/https://www.ultraviolet.rs/blog/tee-tls-privacy/
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
