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
fDate :
10/1/1997 12:00:00 AM
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;
Journal_Title :
Software Engineering, IEEE Transactions on
