Security protocols are small distributed programs which aim to achieve security properties such as confidentiality, authentication, anonymity, etc. Nowadays, security protocols are omnipresent in our daily lives: home-banking, electronic commerce, mobile phones, etc. However, because these protocols are generally implemented on potentially insecure networks (e.g. the Internet) they are extremely difficult to devise. Using Roger Needham's words “Security protocols are three line programs that people still manage to get wrong”. Based on the seminal work of Dolev and Yao, symbolic methods for analyzing such protocols have been in development for about 25 years. The main components of these models are the perfect cryptography assumption and an unbounded non-deterministic adversary that has complete control of the network.

The field of symbolic analysis of security protocols has seen significant advances during the last few years. We now have a better understanding of decidability and complexity questions and models with solid theoretical foundations have been developed together with proof techniques. Automated tools have also been designed and successfully applied to numerous protocols, including industrial protocols, for the provision of security or the discovery of attacks, and models have been extended with algebraic properties in order to weaken the perfect cryptography assumption. Recently, even computational soundness results towards cryptographic models have been achieved.

However, the field was still missing a book which summarized the state-of-the-art of these advances. While we certainly do not pretend to give a complete overview of the field, which would be impossible in a single book, nevertheless, we believe that we have covered a representative sample of the ongoing work in this field, which is still very active. This book contains an introduction and 10 tutorial-like chapters on selected topics, each written by a leading expert in the field of formal analysis of security protocols. We are extremely grateful to all the authors for their hard work and effort in preparing these chapters.

January 2011

Véronique Cortier and Steve Kremer