DocumentCode
1371571
Title
Using CSP to detect errors in the TMN protocol
Author
Lowe, Gavin ; Roscoe, Bill
Author_Institution
Dept. of Math. & Comput. Sci., Leicester Univ., UK
Volume
23
Issue
10
fYear
1997
fDate
10/1/1997 12:00:00 AM
Firstpage
659
Lastpage
669
Abstract
We use FDR (Failures Divergence Refinement), a model checker for CSP, to detect errors in the TMN protocol (M. Tatebayashi et al., 1990). 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
Keywords
communicating sequential processes; cryptography; formal verification; program verification; protocols; CSP processes; FDR; Failures Divergence Refinement; TMN protocol; communicating sequential processes; error detection; general intruder; model checker; security breaches; Algebra; Authentication; Communication system security; Cryptographic protocols; Cryptography; Mobile communication; Redundancy; State-space methods; Testing;
fLanguage
English
Journal_Title
Software Engineering, IEEE Transactions on
Publisher
ieee
ISSN
0098-5589
Type
jour
DOI
10.1109/32.637148
Filename
637148
Link To Document