Using CSP to detect errors in the TMN protocol

被引：87

作者：

Lowe, G ^{[1
]}

Roscoe, B ^{[1
]}

机构：

[1] UNIV OXFORD, COMP LAB, OXFORD OX1 3QD, ENGLAND

来源：

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING | 1997年 / 23卷 / 10期

关键词：

security protocols; key establishment; CSP; FDR; model checking; cryptography; protocol failure;

D O I：

10.1109/32.637148

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

In this paper we use FDR, a model checker for CSP, to detect errors in the TMN protocol [18]. We model the protocol and a very general intruder as CSP processes, and use the model checker to test whether the intruder can successfully attack the protocol. We consider three variants on the protocol, and discover a total of 10 different attacks leading to breaches of security.

引用

页码：659 / 669

页数：11

共 18 条

[1]

[Anonymous], 1996, LNCS

[2]

COPPERSMITH D, 1996, LECT NOTES COMPUTER, V1070

[3]

ECKMANN ST, 1985, ACM SOFTWARE ENG NOT, V10

[4]

Formal Systems (Europe) Ltd, 1997, FAIL DIV REF FDR 2 U

[5]

Hoare C., 1985, COMMUNICATING SEQUEN

[6]

Kemmerer R., 1994, J CRYPTOLOGY, V7

[7]

Lowe G, 1996, SOFTWARE-CONC TOOL, V17, P93

[8] Casper: A compiler for the analysis of security protocols [J].

Lowe, G .

10TH COMPUTER SECURITY FOUNDATIONS WORKSHOP, PROCEEDINGS, 1997, :18-30

[9] The NRL protocol analyzer: An overview [J].

Meadows, C .

JOURNAL OF LOGIC PROGRAMMING, 1996, 26 (02) :113-131

[10]

MILLEN JK, 1987, IEEE T SOFTWARE ENG, V13

← 1 2 →