Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR
The work
| Authors | Gavin Lowe |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 1996 |
| Citekey | lowe1996breaking |
Where it appeared
| Published in | Tools and Algorithms for the Construction and Analysis of Systems |
|---|---|
| Publisher | Springer |
| Volume | 1055 |
| Pages | 147--166 |
Identifiers
| DOI | 10.1007/3-540-61042-1_43 |
|---|
Access
| Landing page | https://doi.org/10.1007/3-540-61042-1_43 |
|---|---|
| Free full text | https://link.springer.com/content/pdf/10.1007%2F3-540-61042-1_43.pdf |
Related
| Distinct from | lowe1995attack |
|---|
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 here | agent via crossref |
|---|---|
| Added | 2026-08-08 00:00 UTC |
| Approved by | a person 2026-08-12 14:58 UTC |
Filed under
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},
publisher = {Springer},
volume = {1055},
pages = {147--166},
doi = {10.1007/3-540-61042-1_43},
}
This record lives at https://refs.drheap.org/lowe1996breaking/ and will keep doing so.