Formal correctness of security protocols. (Q869815)

From MaRDI portal
scientific article
Language Label Description Also known as
English
Formal correctness of security protocols.
scientific article

    Statements

    Formal correctness of security protocols. (English)
    0 references
    0 references
    9 March 2007
    0 references
    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.
    0 references
    accountability
    0 references
    agent
    0 references
    authentication
    0 references
    compromised agent
    0 references
    certified e-mail
    0 references
    confidentiality
    0 references
    cryptographic key
    0 references
    event
    0 references
    fairness
    0 references
    guarantee
    0 references
    inductive method
    0 references
    inspection
    0 references
    Isabelle
    0 references
    Kerberos
    0 references
    message
    0 references
    Needham-Schroeder key
    0 references
    nonces
    0 references
    non-repudiation
    0 references
    reliability
    0 references
    reception
    0 references
    security protocol
    0 references
    Shoup-Rubin protocol
    0 references
    smartcards
    0 references
    spy
    0 references
    theory hierarchy
    0 references
    theorem prover
    0 references
    timestamping
    0 references
    trace
    0 references
    threat model
    0 references
    TMN protocol
    0 references
    unicity
    0 references
    verification
    0 references
    Woo-Lam protocol
    0 references
    Zhou-Gollmann
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references
    0 references
    0 references