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
