NSL-lean

Needham-Schroeder in Lean 4, both halves of it: the original protocol is broken here, and Lowe's fix is proved secure.

Two results, and they point in opposite directions:

• NS.lowes_attack — a constructive proof that the original protocol reaches an unsafe state. We exhibit the four-step trace and Lean checks that every step is legal and that Charlie ends up holding Bob's nonce.
• NSL.final_theorem — a proof that with Lowe's fix, in any reachable state where Bob has finished a run he believes is with Alice, the attacker cannot derive Nb. This one is universally quantified over traces, by induction on the reachability relation.

The second proof is axiom-free. #print axioms NSL.final_theorem reports only propext, Classical.choice and Quot.sound — the two protocol facts one is tempted to assume (freshness, and integrity of message 2) are proved instead.

Layout

File	What's in it
NSLLean/Basic.lean	Shared model: agents, nonces, keys, the Message term algebra, the attacker's initKnowledge, and the Dolev-Yao CanDeduce rules
NSLLean/NS.lean	The original protocol and lowes_attack
NSLLean/NSL.lean	Lowe's fix, the secrecy invariant, and final_theorem
report/report.tex	Project report

Both protocols reuse the same term algebra and the same attacker, so the only difference between them is the Step relation — which is exactly where the flaw and the fix live.

Building

lake exe cache get     # first time only, fetches the Mathlib build cache
lake build

Lean 4.29.0-rc1 with Mathlib, pinned in lean-toolchain and lake-manifest.json.

To build the report:

cd report && latexmk -pdf report.tex

How the two proofs work

The attack is a straight-line construction. We name four states s1-s4, prove Step between consecutive ones, and chain them with Relation.ReflTransGen.head. The interesting premises are the CanDeduce obligations: Charlie has to actually build each message he injects, so we derive {Na, A}_Pub(B) by decrypting Alice's message 1 with his own private key and re-encrypting the pair for Bob. CanDeduce.mono and the mono_r tactic handle the bookkeeping as the knowledge set grows.

The security proof is an inductive invariant on Reachable. Two message predicates carry it:

• NonceAbsent n m — n does not occur in m at all, not even under encryption. It survives every deduction rule with no assumption about keys, which is what makes freshness provable rather than assumed: a nonce the attacker delivers inside a ciphertext must already have been spent.
• NonceProtected n m — m gives the attacker no route to n. Under a dishonest key the payload has to be protected itself; under an honest key it may instead be one of the two things an honest agent legitimately sends while n is secret, namely a message 2 (Na, n, B) naming an honest B, or the message 3 payload n. Recording which payloads an honest key may carry is what replaces an integrity axiom for message 2 — the aliceFin case inverts it instead of assuming it.

Scope

WorldState has one session slot per honest agent, and no rule ever puts a slot back. NSL.Step.rank_lt and NSL.WorldState.rank_le make this precise: a progress rank rises strictly at every step and never passes 4, so a run is at most four steps — one initiator session for Alice, one responder session for Bob.

That is enough to express Lowe's attack, which is exactly this configuration. It does not cover two concurrent sessions in the same role. Lifting that means replacing the two slots with a Finset of sessions; the message-level lemmas would carry over untouched, only the Step rules and the two state-slot invariants would need reworking.