Issue No. 09 - September (1998 vol. 24)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.713329
<p><b>Abstract</b>—This paper presents a general approach for analysis and verification of authentication properties using the theory of Communicating Sequential Processes (CSP). The paper aims to develop a specific theory appropriate to the analysis of authentication protocols, built on top of the general CSP semantic framework. This approach aims to combine the ability to express such protocols in a natural and precise way with the ability to reason formally about the properties they exhibit. The theory is illustrated by an examination of the Needham-Schroeder Public-Key protocol. The protocol is first examined with respect to a single run and then more generally with respect to multiple concurrent runs.</p>
Authentication, security protocols, formal methods, CSP, verification, Needham-Schroeder protocol.
S. Schneider, "Verifying Authentication Protocols in CSP," in IEEE Transactions on Software Engineering, vol. 24, no. , pp. 741-758, 1998.