Hi Russ, TLS WG:

I had intended to reply on this topic a long time ago but somehow forgot.

I wonder if you have checked Noise Explorer handshake patterns: https://noiseexplorer.com/patterns/.

I think it covers all the different PSK-based handshake patterns: Npsk0, Kpsk0, Xpsk1, NNpsk0, NNpsk2, NKpsk0, NKpsk2, NXpsk2, XNpsk3, XKpsk3, XXpsk3, KNpsk0, KNpsk2, KKpsk0, KKpsk2, KXpsk2, INpsk1, INpsk2, IKpsk1, IKpsk2, IXpsk2.

Perhaps one of them reflects your scenario. Possibly KKpsk0?

Noise explorer comes with pre-written ProVerif models (including active and passive attacker) for each handshake pattern. As a side note, it also includes implementation of the handshake in Go and Rust. For example, on this page: https://noiseexplorer.com/patterns/KKpsk0/, you can find the ProVerif models of the KKpsk0 handshake patterns.

I guess there are subtle differences since Noise Framework is built for DH keys (and not signing keys as in TLS). Also, the certificate verification is not modeled and instead it is assumed that initiator and the responder know the long-term static key of the other party out-of-band. Anyhow, maybe you find it useful for progressing your draft.

--Mohit

On 5/31/24 17:44, Russ Housley wrote:
Usama:

During WG Last Call, several people asked for formal analysis,  I reached out to one researcher to see if thet formal analysis could be provided in response.  I was told the additions were too simple to get a published paper.  So, nothing happened.

This response says that formal analysis is needed to advance rfc8773bis to the Standards Track.  Other documents in other working groups are using RFC 8773,  They are proceeding with a downward reference (that needs to be called out when they reach IETF Last Call).  This means that people are implementing RFC 8773.

I'll gladly work with you or anyone else on the formal analysis.

Russ


On May 31, 2024, at 4:53 AM, Muhammad Usama Sardar <muhammad_usama.sar...@tu-dresden.de> wrote:
I see much more need for analysis when it comes to the authentication properties of the PSK (psk/cert combination), whereas the secrecy (assuming authentication is a non-goal) is much more straightforward.

Who will perform this analysis?  I asked a researcher to perform such an analysis, and the response was that it is too simple to get a paper.  Now waht?

Russ, if you absolutely find no one, I will be happy to work on it over the weekends (so it will be slow). Also to clarify, I prefer to work with ProVerif because in my initial experiments, ProVerif was always way faster than Tamarin.
For the authentication analysis, I think here a Tamarin-like analysis might be useful for checking undesirable interactions; for example, could anything go wrong if a single PSK is used both as a traditional PSK but also as an external PSK?

Here is why I would like to see at least name of the panelist who wrote this. If it is Cas, it makes perfect sense to me. If it is someone else, I would like to know why he would prefer to recommend Tamarin over ProVerif. What exactly is missing in ProVerif that would make it unsuitable for this analysis? Or is it some usability issue?

Best Regards,

Usama



_______________________________________________
TLS mailing list --tls@ietf.org
To unsubscribe send an email totls-le...@ietf.org
_______________________________________________
TLS mailing list -- tls@ietf.org
To unsubscribe send an email to tls-le...@ietf.org

Reply via email to