Formal correctness of security protocols. (Q869815)

This book is a very technical treatment of protocol security issues. By its content, the book addresses the software development theorists interested in both modelling and automatic verification of security protocols. The author was involved with the inductive method and the theorem prover Isabelle even from their inception. The present text, originating from the author's Ph.D. thesis, includes a valuable contribution devoted to apply the inductive method for verifying properties of real-world communication protocols. The inductive method is the key technique extensively used for treating formally the properties of real-size protocols. The method's principles and its environment, namely the theorem prover Isabelle, are gradually presented, starting from Chapter 3. Chapter 4 formalizes within the inductive method seven groups of guarantees for protocol models: reliability, regularity, authenticity, unicity, confidentiality, authentication, key distribution. Chapter 5 defines a new principle, called goal availability, offering a valuable complement to the existing design principles for the common aim of strengthening protocols. Chapters 6 and 7 extend the inductive method with a treatment of timestampings, modelled as guessable numbers, in order to analyse protocols like BAN Kerberos and Kerberos IV. Chapter 8 provides a formal definition of the agents' knowledge of messages and message components in order to provide support for verifying the key distribution goal and to make the inductive method strong enough for analyzing new hierarchies of protocols. Chapter 9 reports on the formal analysis of the most recent version of the Kerberos protocol. It is verified that the removal of the use of double encryption in Kerberos V does not significantly influence the protocol goals. Chapters 10 and 11 deal with the analysis of smartcards-based protocols. The extended inductive method is applied to Shoup-Rubin, and it is shown that this protocol violates confidentiality, authentication and key distribution goals. The drawback is fixed by the author by designing a new variant protocol. Chapter 12 further adds to the inductive method new capabilities making it able to modelling and verifying accountability protocols. These extensions are used next in Chapter 13 to describe the analysis of two forms of accountability, namely non-repudiation and certified e-mail delivery. It is proved that both protocols are fair and deliver valid evidence. Chapter 14 highlights the author's contribution through its key concepts. The interested computer scientist might find here valuable hints for future important developments in specifying and verifying secure network communication protocols. Even if the exposition is meticulous and very rigorous and the book is fairly self-contained, the understanding of the main approaches requires a solid background in cryptographic protocols and inductive reasoning about software properties.