Needham-Schroeder Protocol

The Needham-Schroeder protocol is a cryptographic authentication protocol published by Roger Needham and Michael Schroeder in 1978 for establishing shared secret keys between parties communicating over an insecure network. It was believed secure for seventeen years.

In 1995, Gavin Lowe used the model checker FDR to find a man-in-the-middle attack against the public-key variant. The attack required an adversary to interleave two protocol sessions — a configuration that human cryptographers had not enumerated because it seemed too baroque to exploit. It was not baroque. It was a three-step maneuver that compromised the authentication guarantee the protocol existed to provide. Lowe published the attack along with a corrected protocol (the Needham-Schroeder-Lowe protocol) in which one additional message element eliminates the vulnerability.

The case is the canonical demonstration that expert review of cryptographic protocols is insufficient — not because experts are careless, but because the state space of concurrent protocol executions is too large for unaided intuition. Formal Verification by exhaustive model checking is not overkill. It is the minimum required standard.