The Modelling and Analysis of Security Protocols: the CSP Approach

9.2. The Dolev-Yao model

A significant early step in the development of the subject was the 1983 paper of Dolev and Yao [25]. This laid the conceptual foundations of the subject by presenting the basic intruder model that has been used in virtually all the work since, including our own. Here the idea of an intruder with the ability to manipulate messages passing over the system – deleting, replaying, faking, redirecting, and so on, limited only by the cryptographic constraints – was set out. The paper also introduced the idea of viewing the problem as a form of word problem.