Why Informal Proofs Are Not Enough

Protocol designers routinely produce informal security arguments — prose reasoning about why an attacker cannot succeed. History shows these arguments are frequently wrong, even for expert-designed protocols.

Needham-Schroeder (1978) was designed for mutual authentication. In 1995, Gavin Lowe found a man-in-the-middle attack using automated verification — 17 years after publication. The informal proof missed a subtle replay.