Subject: Formal analysis of Kerberos 5

From: Aaron Jaggard <[email-masked]>
Date: Mon, 26 Apr 2004 20:31:57 -0500

Dear colleagues,

    Below are links to a technical report describing a formal analysis of
Kerberos 5 (joint work with F. Butler, I. Cervesato, and A.
Scedrov); this elaborates on an shorter workshop paper and
addresses comments from the working group on that work.  We would
welcome any additional comments on the extended version.

    Best regards,   Aaron Jaggard

.pdf file:
    ftp://ftp.cis.upenn.edu/pub/papers/scedrov/ms-cis-04-04.pdf

.ps file:
    ftp://ftp.cis.upenn.edu/pub/papers/scedrov/ms-cis-04-04.ps

Abstract:

We give three formalizations of the Kerberos 5 authentication
protocol in the Multi-Set Rewriting (MSR) formalism.  One is a
high-level formalization containing just enough detail to prove
authentication and confidentiality properties of the protocol.  A
second formalization refines this by adding a variety of protocol
options; we similarly refine proofs of properties in the first
formalization to prove properties of the second formalization. Our
third formalization adds timestamps to the first formalization but
has not been analyzed extensively.  The various proofs make use of
rank and corank functions, inspired by work of Schneider in CSP,
and provide examples of reasoning about real-world protocols in
MSR.  We also note some potentially curious protocol behavior;
given our positive results, this does not compromise the security
of the protocol.