Hi All, I'm an implementer (Verified Infrastructure Response Protocol, draft-howard-virp), not a regular on this list, but I wanted to share a data point on the value of formal analysis engagement for individual-submission authors.
Usama reviewed VIRP's cryptographic core and helped guide the formal verification work. We machine-verified HMAC key secrecy and non-injective agreement in both ProVerif and Tamarin under Dolev-Yao, establishing G1 mod EUF-CMA. That result is now cited in draft-howard-virp-05 ยง16.1 and meaningfully strengthened the draft. For anyone interested, the discussion happened publicly and is archived: https://mailarchive.ietf.org/arch/search/?q=virp I'm not in a position to comment on the specific process changes proposed in -07. I can say that without accessible formal-methods engagement, an independent author like me would not have gotten this kind of review, and the draft would be weaker for it. Whatever process the WG lands on, preserving that pathway for non-affiliated implementers seems worth keeping in view. Thanks to Usama and the FATT contributors. Best, Nate Howard Third Level IT
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
