Formal correctness of security protocols.
type: Item
instance of: scholarly article
title: Formal correctness of security protocols.
zbMATH Open document ID: 1176.68026
author: Giampaolo Bella
published in: Information Security and Cryptography
publication date: 2007-03-09T00:00:00Z
review text: 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, authen…
reviewed by: Tudor Bălănescu
Mathematics Subject Classification ID: 68M12
Mathematics Subject Classification ID: 68-02
Mathematics Subject Classification ID: 68M10
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 94A60
Mathematics Subject Classification ID: 94A62
zbMATH DE Number: 5132531
zbMATH Keywords: accountability
zbMATH Keywords: agent
zbMATH Keywords: authentication
zbMATH Keywords: compromised agent
zbMATH Keywords: certified e-mail
zbMATH Keywords: confidentiality
zbMATH Keywords: cryptographic key
zbMATH Keywords: event
zbMATH Keywords: fairness
zbMATH Keywords: guarantee
zbMATH Keywords: inductive method
zbMATH Keywords: inspection
zbMATH Keywords: Isabelle
zbMATH Keywords: Kerberos
zbMATH Keywords: message
zbMATH Keywords: Needham-Schroeder key
zbMATH Keywords: nonces
zbMATH Keywords: non-repudiation
zbMATH Keywords: reliability
zbMATH Keywords: reception
zbMATH Keywords: security protocol
zbMATH Keywords: Shoup-Rubin protocol
zbMATH Keywords: smartcards
zbMATH Keywords: spy
zbMATH Keywords: theory hierarchy
zbMATH Keywords: theorem prover
zbMATH Keywords: timestamping
zbMATH Keywords: trace
zbMATH Keywords: threat model
zbMATH Keywords: TMN protocol
zbMATH Keywords: unicity
zbMATH Keywords: verification
zbMATH Keywords: Woo-Lam protocol
zbMATH Keywords: Zhou-Gollmann
describes a project that uses: Casper
MaRDI profile type: Publication
description: scientific article; zbMATH DE number 5132531