While this is worthwhile, there is an opportunity for the math to violate your assumptions in a way you didn't understand. Let's talk briefly about TLS 1.3 Selfie attacks.
TLS 1.3 is the first TLS in which experts built a formally verified model of the protocol before they shipped the standard. There are models of earlier TLS versions, but nothing learned from them could be incorporated into the corresponding standard because they were an afterthought - like writing unit tests after shipping version 1.0
TLS 1.3 has a mode intended for applications where some nodes which have a pre-existing relationship communicate, in this case we don't need the Web PKI ("SSL certificates") instead we use Pre-shared Keys (PSKs) - that is all the parties know the keys anyway, which clearly couldn't work for the open web but is fine for my boiler and its remote thermostat since duh, I don't want some random other person's thermostat talking to my boiler. PSKs are also used when you connect to the same server again later, but that doesn't matter here.
The mathematical proof seemed to say exactly what the designers wanted, and it passed. So TLS 1.3 is exactly what we wanted... right? Well, almost. Designers were thinking of symmetries like "Alice talks to Bob" and "Bob talks to Alice" as one conversation, but the proof thinks that's two conversations. So the proof thinks Alice and Bob need two keys, the Alice->Bob key and the Bob->Alice key, while humans assumed they only need a single key, an Alice-x-Bob key. And so the RFC documents (prior to errata) the human assumption but the protocol actually requires the machine assumption.
The result is the Selfie Attack. In our scenario Alice, and Bob have a Cat. The Cat, like many cats, would like more food, but Alice and Bob use a secure protocol to ensure they only feed the cat once.
Bob has fed the cat and left. The cat is sat by an empty food bowl looking plaintive. Alice sends Bob an encrypted message, "Did you feed the cat?". The Cat intercepts the message, it doesn't have the Alice-x-Bob key so it can't decrypt this message nor directly answer it, but it doesn't need to. The Cat simply sends Alice's own message back to her. Receiving a message encrypted with the Alice-x-Bob key, Alice concludes it's from Bob. "Did you feed the cat?". So she replies "No, I did not feed the cat". The cat receives this message too, and directs it back to Alice as well, now Alice has what appears to be a reply to her first question, "No, I did not feed the cat" encrypted with the Alice-x-Bob key. So, Alice feeds the cat again because the cat was able to trick her into answering her own question.
I like your simplified example, but it does miss an important nuance: Alice has to act as both a client and a server, must use the same PSK for both roles, and must not (or not be able to) check the sender or intended recipient of any message.
TLS handshakes were never designed to be symmetric. Every TLS connection is clearly between a client and a server. Alice and Bob, both running a client and a server, where both servers use the same PSK, is not a TLS setup. It's two (2) separate TLS setups.
The math was never intended to verify if sharing PSKs across independent unrelated servers is safe. In fact, the Selfie attack is not really a "selfie" attack; it works even if Alice hosts only a client and no server, as long as there exists an Eve that hosts a server (but not necessarily a client).
> Designers were thinking of symmetries like "Alice talks to Bob" and "Bob talks to Alice" as one conversation ...
I strongly doubt that. A TLS connection, once established, is symmetric, sure, but a TLS handshake isn't. The failure mode in Selfie isn't in the post-handshake domain. It's not like Selfie allows you to take packets from an already established connection and play it against an unsuspecting server that has no connections, and thus making it think it has a connection.
The failure is literally this: Alice says "Hey I wanna talk to you" intended for Bob but doesn't specify who, exactly, are "I" and "you". The Cat records Alice's speech and replays it to her, making her believe someone is trying to initiate a new, separate conversation.
The verifiers writing the proofs would be acutely aware of the asymmetrical nature of TLS handshakes. In fact, I strongly doubt they even considered any case where the same entity hosts both a TLS client and a TLS server for a shared purpose.
This is Hacker News, where people who know nothing about a topic come to tell each other about their expertise. You believe no-one would make this type of mistake, I know they did and I have just provided you a link to the paper at the time. Alas some people will believe you, and they will assume that they too are infallible and the rest is inevitable.
Thank you for reminding me to read the original report again. However, I still don't see any evidence to support your claim that the designers assumed TLS connections to be symmetric in their establishment.
Maybe I'm reading the report differently from you, or maybe I'm misreading it or missing sth — though I did honestly try to read it from your perspective — but I just don't see anything in the report where session establishment or resumption ignores the role of a participant. A client is still a client that cannot receive new connections and a server is still a server that cannot initiate connections.
The report does support my reading of the issue though:
1. That Selfie would not be possible if a server checked the intended recipient of any handshake message it received; and
2. That Selfie would not be possible if the assumption that a PSK is a secret known only to one client and one server were not violated. How it is violated — whether by reusing the client and server host nodes and deploying the opposite roles on each (your symmetric case), or by setting up two extra, completely unrelated and independent host nodes (no symmetry here) — does not matter. They are both violations of secrecy of PSK and thus vulnerable to Selfie either way.
----
> You believe no-one would make this type of mistake
I did not "believe no-one would". I "strongly doubted" (which is subtly, but importantly enough, different from belief) whether a proof writer who's intimately familiar with TLS handshake (again, not "no-one") "would".
> Alas some people will believe you, and they will assume that they too are infallible and the rest is inevitable.
I ... don't see where this is going. Or why.
> What did Dorothy Parker say about Horticulture ?
Okay, you've definitely lost me.
----
Look, I'm not arguing that mathematical proofs are infallible to modeling inaccuracies, or that they should be trusted blindly. Or that people can be perfect if they have enough expertise. Absolutely not. I only disagreed on some nuances of the specific example you provided.
But you may not be interested in that. Especially given how you generalised my words above (and thus erased them of all nuance), I'm going to read the signs I see, write this whole thing off as basically an exercise in pedantry, and end this here.
Thanks for your example. I am not very familiar with it, so I learned a few things.
I guess I see the point of OPs question now.
The formal verification can only prove that something works according to a specification, not that it (or the specification) does what x stakeholder wanted.
In this sense, it makes the error surface smaller, but does not remove it.
TLS 1.3 is the first TLS in which experts built a formally verified model of the protocol before they shipped the standard. There are models of earlier TLS versions, but nothing learned from them could be incorporated into the corresponding standard because they were an afterthought - like writing unit tests after shipping version 1.0
TLS 1.3 has a mode intended for applications where some nodes which have a pre-existing relationship communicate, in this case we don't need the Web PKI ("SSL certificates") instead we use Pre-shared Keys (PSKs) - that is all the parties know the keys anyway, which clearly couldn't work for the open web but is fine for my boiler and its remote thermostat since duh, I don't want some random other person's thermostat talking to my boiler. PSKs are also used when you connect to the same server again later, but that doesn't matter here.
The mathematical proof seemed to say exactly what the designers wanted, and it passed. So TLS 1.3 is exactly what we wanted... right? Well, almost. Designers were thinking of symmetries like "Alice talks to Bob" and "Bob talks to Alice" as one conversation, but the proof thinks that's two conversations. So the proof thinks Alice and Bob need two keys, the Alice->Bob key and the Bob->Alice key, while humans assumed they only need a single key, an Alice-x-Bob key. And so the RFC documents (prior to errata) the human assumption but the protocol actually requires the machine assumption.
The result is the Selfie Attack. In our scenario Alice, and Bob have a Cat. The Cat, like many cats, would like more food, but Alice and Bob use a secure protocol to ensure they only feed the cat once.
Bob has fed the cat and left. The cat is sat by an empty food bowl looking plaintive. Alice sends Bob an encrypted message, "Did you feed the cat?". The Cat intercepts the message, it doesn't have the Alice-x-Bob key so it can't decrypt this message nor directly answer it, but it doesn't need to. The Cat simply sends Alice's own message back to her. Receiving a message encrypted with the Alice-x-Bob key, Alice concludes it's from Bob. "Did you feed the cat?". So she replies "No, I did not feed the cat". The cat receives this message too, and directs it back to Alice as well, now Alice has what appears to be a reply to her first question, "No, I did not feed the cat" encrypted with the Alice-x-Bob key. So, Alice feeds the cat again because the cat was able to trick her into answering her own question.