Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR

The work

AuthorsGavin Lowe
Typeinproceedings
Year1996
Citekeylowe1996breaking

Where it appeared

Published inTools and Algorithms for the Construction and Analysis of Systems
PublisherSpringer
Volume1055
Pages147--166

Related

Distinct fromlowe1995attack The 1995 Information Processing Letters note states the attack on the Needham-Schroeder public-key protocol; the 1996 TACAS paper gives the fuller treatment and the fix, and adds the mechanical check that found it. Same result, two documents a year apart, neither a reprint of the other. Cite the first for priority and the second for the method.

Abstract

In this paper we analyse the well known Needham-Schroeder Public-Key Protocol using FDR, a refinement checker for CSP. We use FDR to discover an attack upon the protocol, which allows an intruder to impersonate another agent. We adapt the protocol, and then use FDR to show that the new protocol is secure, at least for a small system. Finally we prove a result which tells us that if this small system is secure, then so is a system of arbitrary size.

A copy is held

pdf, 941.2 kB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereagent via crossref
Added2026-08-08 00:00 UTC
Approved bya person 2026-08-12 14:58 UTC

Cite it as

@inproceedings{lowe1996breaking,
  title        = {Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR},
  author       = {Gavin Lowe},
  year         = {1996},
  booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems},
  volume       = {1055},
  pages        = {147--166},
  publisher    = {Springer},
  doi          = {10.1007/3-540-61042-1_43},
}

This record lives at https://refs.drheap.org/lowe1996breaking/ and will keep doing so.