This is a compilation of selected tutorial papers from the 2007 to 2009 Foundations of Security Analysis and Design (FOSAD) schools. In the first paper, Escobar, Meadows, and Meseguer describe the Maude-NRL protocol analyzer (Maude-NPA), a model-checking tool. Many researchers use formal methods to analyze cryptographic protocols--an approach that emphasizes automated machine specification and analysis--so this tool is very relevant.

The sixth paper in this collection, “The open-source fixed-point model checker for symbolic analysis of security protocols,” is closely related to the first paper. Mödersheim and Luca Viganò describe the on-the-fly model checker (OFMC), another model-checking tool for symbolic cryptographic protocol analysis. Also related, Rustan et al.’s paper describes Chalice, a language and program-verifier tool.

In the second paper, Barthe and Kunz briefly introduce certificate translation, the underlying principles of proof-carrying code, and the source programming language.

In the next paper, Chadwick introduces federated identity management (FIM), a topic that will interest both researchers and practitioners. With FIM, organizations can securely share confidential user identities. The paper briefly introduces the seven laws of identity and some of the privacy issues associated with identity management systems, and uses two early FIM systems as case studies. As an example, Chadwick describes the key drivers that most probably result in a slow adoption (or scaling back) of the two early FIM systems. He also describes two existing FIM systems in some detail.

Jacobs and Pieters outline the history of the Netherlands’ traditional and electronic voting system and its underlying principles and techniques. They attempt to explain why e-voting has failed to take off in the Netherlands, despite the country being an early adopter. The other four papers in the book cover topics such as access and authorization control, and wireless security.

This collection is an excellent resource for computer science (CS) graduate students, scholars, and practitioners interested in security-related research. Furthermore, it provides up-to-date citations for further study. Not surprisingly, the reader is expected to possess a strong mathematics background.

The organization of the book could use some improvement. The book is divided into three main parts: “FOSAD 2007,” “FOSAD 2008,” and “FOSAD 2009.” It would be more helpful for the reader if related topics were compiled together, rather than grouped by year. For example, Part 1 should include all the papers on cryptographic protocol analysis, even though they are from different FOSAD schools.