Hi D. J. Bernstein,Focusing only on two points for now. I'll do further working on the formal modeling and research for the rest and share with the WG later, or ask you for further clarifications, if required.
Respectfully, I would like to kindly request that you maintain the professional respect that John deserves as a long-standing contributor of TLS. He has not only made substantial contributions to the TLS protocol, but also made significant contributions in helping me maintain the proofs for FATT. Some that I remember off-hand are describing the detailed scenarios for key reuse for formal modeling, and at several occasions, he has provided me substantial technical responses with concrete references for further research and formal modeling.
Perhaps rather just forget about John. I have shared my independent analysis in [0] of why he is right. FWIW, I believe TLS is broader than just the Web. IMHO, firewalls using TLS certificates is also part of TLS ecosystem. TLS WG did spend a lot of energies in middle boxes. I haven't seen any rebuttal in your email to my points on firewalls in [0]. We haven't modeled firewalls and middle boxes in our formal models, which is a pity, otherwise I could say with more confidence, but as I said in [0], I don't see intuitively what's wrong. Please tell me explicitly what's wrong in my firewall reasoning in [0].
===Second, I am really surprised that I am repeatedly being pointed to a 13-years old attack as an attestation that my formal proofs are 'advertised' and 'marketing.' I have no objection to these labels as long as you justify these claims. So please do justify.
Quoting below as per your permission in [1]: On 07.06.26 12:41, D. J. Bernstein wrote:
Huh?
This tone is not really respectful.
My reading is slightly different. ISTM the specific dispute being discussed has been reconciled in [0]. I don't see anyone other than you disputing my reconciliation in [0]. As per AD instruction, the discussion should happen at TLS. I am not a member of various lists that you keep adding. So if I have missed something on these lists, please let me know.Important disputes remain unresolved.
I appreciate the concern. I would be happy if you could share concrete feedback on the artifacts[2] to make them more comprehensive.Those are symbolic analyses. As I wrote before: Symbolic analyses habitually use computers (good) but unfortunately do this by skipping not just quantification but many other cryptographic details---and we know quite a few examples such ashttps://cr.yp.to/papers.html#rc4biases where feasible TLS attacks were allowed by those details.
FWIW, I view symbolic and computational methods as /complementary/, as I mention in [4]. Putting in all cryptographic details in the symbolic model defeats the entire purpose of symbolic analysis.
If you label my formal proofs as 'advertised' and 'marketing,' please justify the claim by showing concrete problems in my proofs [2], beyond the already known attacks [3], and constructively contribute by proposing the fixes to those problems.
Thanks in advance for your valuable contributions to formal proofs. Best regards, -Usama [0] https://mailarchive.ietf.org/arch/msg/tls/gyqsw9W5YUX-ySRfkisv3zNPcdY/[1] https://mailarchive.ietf.org/arch/msg/last-call/oKrCjFfDUYoePOVSyWQ-URQU9Fk/
[2] https://github.com/CCC-Attestation/formal-spec-id-crisis [3] https://mailarchive.ietf.org/arch/msg/tls/8lyqHh9y7_Lv6b1iXhpUqYrp0M0/[4] https://www.ietf.org/archive/id/draft-usama-tls-risks-of-mlkem-02.html#section-2-3
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
