• “The more complex the threats become, the more you have to do the basics and groundwork really well. Staying aware and on top of new vulnerabilities and ensuring that patches and software updates are rapidly implemented is crucial.”

    Jeff Shipley, Cisco Intelligence Collection Manager, Cisco 2008 Annual Security Report

    Read more...
  • The software security industry today is at about the same stage as the auto industry was in 1930" ... "it looks fast, goes nice but in an accident you die.” ... "The major shortfall is absence of assurance (or safety) mechanisms in software. If my car crashed as often as my computer does, I would be dead by now."

    Brian Snow, Former Technical Director of the US National Security Agency (NSA), "We need assurance!", 1999-2008

    Read more...
  • “When will we be secure? Nobody knows for sure – but it cannot happen before commercial security products and services possess not only enough functionality to satisfy customers’ stated needs, but also sufficient assurance of quality, reliability, safety, and appropriateness for use. Such assurances are lacking in most of today’s commercial security products and services.”

    Brian Snow, Former Technical Director of the US National Security Agency (NSA), "We need Assurance", 2005

    Read more...
Home Resources Security bibliography Symmetric key exchange protocols bibliography: Formal analysis of Kerberos 5
bibliography: Formal analysis of Kerberos 5
Authors: Frederick Butler, Iliano Cervesato, Aaron D. Jaggard, Andre Scedrov, Christopher Walstad
Organisation:
Date: November 2006
Keywords: symmetric key exchange, symmetric authentication, Kerberos, federated system, cryptanalysis
Electronic Publication: PDF on CITESEER
Abstract:

We report on the detailed verification of a substantial portion of the Kerberos 5 protocol specification. Because it targeted a deployed protocol rather than an academic abstraction, this multi-year effort led to the development of new analysis methods in order to manage the inherent complexity. This enabled proving that Kerberos supports the expected authentication and confidentiality properties, and that it is structurally sound; these results rely on a pair of intertwined inductions.

Our work also detected a number of innocuous but nonetheless unexpected behaviors, and it clearly described how vulnerable the cross-realm authentication support of Kerberos is to the compromise of remote administrative domains.

Notes: This paper may describe the most effective attacks against Kerberos as of 2008.
Citation: Frederick Butler, Iliano Cervesato, Aaron D. Jaggard, Andre Scedrov, Christopher Walstad, “Formal analysis of Kerberos 5”, Theoretical Computer Science, v.367 n.1, p.57-87, 24 November 2006
Related work:

Last Updated on Sunday, 04 January 2009 11:04