Using CSP to detect errors in the TMN protocol

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. W...

Full description

Saved in:
Bibliographic Details
Published in:IEEE transactions on software engineering 1997-10, Vol.23 (10), p.659-669
Main Authors: Lowe, G., Roscoe, B.
Format: Article
Language:English
Subjects:
Algebra
Applied sciences
Authentication
Communication system security
Computer science
control theory
systems
Cryptographic protocols
Cryptography
Cybersecurity
Data encryption
Exact sciences and technology
Mobile communication
Protocol
Redundancy
Software
Software engineering
State-space methods
Studies
Testing
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0098-5589
1939-3520
DOI:10.1109/32.637148