It is well known that protocols for exchanging cryptographic keys over data networks can be vulnerable to message modification attacks. This fact led to the development of tools for cryptographic protocol analysis. Some of the earlier papers on the subject are [MCF87, Mea91] on goal-directed state search tools implemented in Prolog, [Kem89] on the application of general purpose specification and verification tools, [BAN90] on a specially designed logic of belief, and [Ros95, Low96] on the application of a model-checking tool for CSP specifications.

• report.ps