USING CSP TO DETECT ERRORS IN THE TMN PROTOCOL

Authors
LOWE G ROSCOE B
Citation
G. Lowe et B. Roscoe, USING CSP TO DETECT ERRORS IN THE TMN PROTOCOL, IEEE transactions on software engineering, 23(10), 1997, pp. 659-669
Citations number
18
Categorie Soggetti
Computer Sciences","Engineering, Eletrical & Electronic","Computer Science Software Graphycs Programming
Journal title
IEEE transactions on software engineering → ACNP
ISSN journal
00985589
Volume
23
Issue
10
Year of publication
1997
Pages
659 - 669
Database
ISI
SICI code
0098-5589(1997)23:10<659:UCTDEI>2.0.ZU;2-G
Abstract
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 intru der as CSP processes, and use the model checker to test whether the in truder can successfully attack the protocol. We consider three variant s on the protocol, and discover a total of 10 different attacks leadin g to breaches of security.