Rosenpass – formally verified post-quantum WireGuard

The paper abstract mentions a "cookie"-like concept, and from websec I know that cookies are not always the optimal solution and historically cookie implementations had a lot of attack surface.

EDIT: Seems to come from German Max-Planck Institute which is funded by German government.

"Lacking a reliable way to detect retransmission, we remove the replay protection mechanism and store the responder state in an encrypted cookie called “the biscuit” instead. Since the responder does not store any session-dependent state until the initiator is interactively authenticated, there is no state to disrupt in an attack."

Both WG and PQWG are vulnerable to state disruption attacks; they rely on a timestamp to protect against replay of the first protocol message. An attacker who can tamper with the local time of the protocol initiator can inhibit future handshakes, rendering the initiator’s static keypair practically useless.

The use of the insecure NTP protocol is the reason for the "cookie" / "Biscuit" mechanism.

The question is too broad to be answered, there are many different formal verification techniques (including static formal verification techniques, and also dynamic formal verification techniques which happen at runtime), and you could be formally verifying only specific properties of the system.

Now, if your formal verification technique forces you to check that each index you use is within bounds (for instance, by forcing you to write loop invariants for each loop, but that's not sufficient because you can index buffers outside a loop or with something unrelated to the loop invariant), then yes, you have proved that you will not overflow buffers.

But those pesky implementations are always imperfect and never totally proved correct, what's more they run on pesky hardware which could have flaws and which is usually not itself perfectly verified, so…

And then you have model checking, which is also a formal verification technique. You can prove that you won't overflow buffers… in the model (which is a spec). That proves that your spec is sound and that you can implement it without flaws, but it does not actually check that your implementation is correct, of course. Unless your model checking tool can also build the implementation and this feature is proved correct.

edit: it seems my model checking paragraph is more relevant than I expected, this submission is actually about model checking if it checks the protocol (and not the implementation).