> how did this attack slip through, despite the fact that the 802.11i handshake was formally proven secure?

So, we cannot trust even formal verification?

> it’s a factual statement. In formal analysis, definitions really, really matter!

If lack of definition implies flaws in formal verification, does that mean we need an additional formal verification of formal verification?

Update:

> We need machine-assisted verification of protocols, preferably tied to the actual source code that implements them.

Haskell, here is your opportunity :-)