Issue No. 10 - October (1997 vol. 23)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.637148
<p><b>Abstract</b>—In this paper we use FDR, a model checker for CSP, to detect errors in the TMN protocol [<ref rid="bibe065918" type="bib">18</ref>]. 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.</p>
Security protocols, key establishment, CSP, FDR, model checking, cryptography, protocol failure.
G. Lowe and B. Roscoe, "Using CSP to Detect Errors in the TMN Protocol," in IEEE Transactions on Software Engineering, vol. 23, no. , pp. 659-669, 1997.