Hi Ilari, Thanks for the clarification. You are making good points here.
On 02.05.26 08:46, Ilari Liusvaara wrote:
On Thu, Apr 30, 2026 at 10:27:58PM +0200, Muhammad Usama Sardar wrote:Hi Ilari, In addition, I was a bit surprised to see the word 'dangerous' for which I have a related formal analysis based on which FWIW, I deem what Scott has described to be secure at the /symbolic/ (not /computational/) level. So I would like to understand what I have got wrong in my analysis.Sure, it is secure under some assumptions.
Sure, fully agree.
However: - Do the assumptions hold in practice?
I think we all need to work together to ensure that the assumptions hold in the implementation.
- Is the RP implementing the required policy correctly?
I agree we need to provide guidance on this in the draft.I'll propose some text to authors for this.
I also agree it needs to be more explicit in the formal analysis. Thank you for your help in improving it.
I acknowledge that symbolic analysis has limitations. Has 'dangerous' got something to do with cryptography? Do you recommend getting confirmation via computational proof in tools like CryptoVerif? or do you have an intuition where the proof will break at the computational level?It does not have anything to do with cryptography itself. It is practical design and implementation stuff. Continuing the "poorly thought out or risky designs" comment, those are almost never stuff protocol-level formal analysis would be expected to catch.
As formal methods enthusiast, I view it differently. My perspective is that something which is formally analyzed at /symbolic/ level is less likely to be classified as "poorly thought or risky design." While it is painful effort, it is possible to develop the formal model for the /implementation/ instead of just /specification/. Yes, I'll have to be that 'bad guy' who will keep asking 'irritating' questions to the authors about every nit of how it will be implemented. But I see light at the end of the tunnel. I have provided a concrete counter-example in another thread [0], where a high-severity CVE was eventually found.
IMHO, even if it is, something which will be further cryptographically verified at /computational/ level [1] would be even less likely to be classified as "poorly thought or risky design."
===And just to clarify, I had very intentionally said "Scott's email," which entails his last paragraph. Similar to Scott, I am not tied to any particular solution for hybrid authentication. To the best of my current knowledge, understanding, and belief, both set of authors have put in a lot of honest effort and I have attested to both existing solutions. If you (or someone) will propose another reasonable starting point, I'll attest to that too. And if someone will show me a concrete flaw in my formal analysis, I'll revoke my corresponding attestation too. My point is just to get started with the work on hybrid authentication, and that we need your expertise, and that I will keep encouraging folks to attest to both (or at least one of the) drafts.
===Happy to discuss further if you have very specific points on what to add to the formal analysis, in addition to the RP policy.
Best regards, -Usama [0] https://mailarchive.ietf.org/arch/msg/tls/dafxb9LpBxRaI_wYb0ObC8xqNHY/[1] Someone asked in an off-list discussion about the usage of my 'computational,' so for others who may also find it confusing: I mean it in the sense we use it in formal methods community (e.g., UFMRG): cf. https://eprint.iacr.org/2019/1393.pdf
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
