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.

WEP was approved by the IEEE in 1997 with informal security claims. By 2001, researchers found RC4 key-stream reuse, IV collisions, and lack of integrity — breaking it in minutes. Informal reasoning missed all of it.

Protocol security depends on interactions between many concurrent sessions, active attackers, and cryptographic assumptions. Human reasoning struggles with state explosions and interleaved concurrent executions.

Formal methods model the protocol mathematically and prove — or disprove — security properties (secrecy, authentication, forward secrecy) for all possible attacker strategies, not just those the designer considered.

Symbolic (Dolev-Yao): crypto is perfect black box; focus on protocol logic. Computational: actual probabilistic security games; closer to real-world guarantees. Both catch real bugs.

POODLE (2014) exploited a padding oracle in SSL 3.0 CBC. The vulnerability was a protocol-level design flaw, not an implementation bug. Formal analysis of the SSL 3.0 spec would have flagged the oracle before deployment.

TLS 1.3 (RFC 8446) was designed alongside formal analyses using ProVerif and miTLS. The specification was iterated based on formal findings — a milestone in standards-body adoption of formal methods.

Formal tools verify the protocol model, not the implementation. A formally verified protocol can still have an insecure implementation. F* / HACL* extends verification to cryptographic code itself.

Formal verification is expensive: protocol modelling takes weeks and requires specialised expertise. But for high-value targets (TLS, SSH, Signal), the cost is justified — one protocol flaw can affect billions of users.

What made Lowe's 1995 discovery of the Needham-Schroeder attack significant?

Informal proofs fail because human reasoning misses concurrent-session interactions and attacker strategies. Needham-Schroeder, WEP, and POODLE all had informal security arguments. TLS 1.3 incorporated formal analysis during design. Formal tools catch protocol-level bugs before deployment.