Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR
Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR
复制标题
DOI：
10.1007/3-540-61042-1_43
复制
发表时间：
1996-03
期刊：
影响因子：
--
通讯作者：
G. Lowe
中科院分区：
文献类型：
--
作者：
G. Lowe
在本文中，我们分析了著名的Needham-Schroeder公钥协议使用FDR，细化检查CSP。我们使用FDR来发现对协议的攻击，它允许入侵者冒充另一个代理。我们修改了协议，然后使用FDR来证明新协议是安全的，至少对于一个小系统来说是安全的。最后我们证明了一个结果，它告诉我们，如果这个小系统是安全的，那么一个任意大小的系统也是安全的。
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.