As any field matures, theory and mathematics appear. Security is no exception. Areas such as cryptology have been mathematical for a long time, in fact, it is quite near impossible to any serious work in cryptology without good math knowledge. Other areas in security are in various stages of catch up mode. Protocols are still a bit to low level for many security professionals, but they are the basic building blocks of security. The folks who work with protocols every day understand them in a way that the rest of us do not. The demand for protocol improvements has been increasing for a while, however, there are not a lot of books explaining protocols and even fewer that try to model them. Ryan and Schneider have helped to fill that gap with this book.

The authors use CSP, Communicating Sequential Processes, "...a mathematical framework for the description and analysis of systems consisting of components (processes) interacting via the exchange of as interprocess messages." It is process algebra which operating systems folks will recognize as interprocess communications or task-to-task communication, not a new concept [1, 2], but a somewhat different use. The principle of correct message delivery is at the heart of it.

They also use use a commercial model checker FDR from Formal Systems and a compiler called Casper, written by the authors. All three of these tools are available on the Web. Their process is to describe a protocol in a script written in an abstract notation for Casper. Casper translates the script into code that CSP can read and then can be checked by FDR. The Casper script has several sections that model the protocol, such its description, the variables, the processes, specifications, functions systems and the intruder. Each section is written in a formal manner with a specific syntax. Naturally, you must have thought it through beforehand.

Throughout the book, the Yahalom protocol is used as the object of analysis. Using the same protocol helps to provide a little more clarity, unlike using a different protocol for different examples. Yahalom is well known enough to make it a good choice to tie everything together. There is a good chapter on writing the Casper code with enough detail to allow the reader to learn it such that it can be useful. A completed scripted is contained in an appendix, along with the output.

The authors cover fundamental principles of security, like authentication, non-repudiation, integrity, and so forth with bridges to the modeling aspects. The explanations are understandable, which is not always the case with mathematical works. The book adds to the security field by making the deeper levels of protocol modeling and analysis more accessible.