nexoncn.com

文档资料共享网 文档搜索专家

文档资料共享网 文档搜索专家

当前位置：首页 >> >> Cryptographically sound security proofs for basic and public-key kerberos

Cryptographically Sound Security Proofs for Basic and Public-Key Kerberos

M. Backes1, I. Cervesato2 , A.D. Jaggard3, A. Scedrov4 , and J.-K. Tsay4

Saarland University backes@cs.uni-sb.de 2 Deductive Solutions iliano@deductivesolutions.com 3 Tulane University adj@math.tulane.edu 4 University of Pennsylvania {scedrov, jetsay}@math.upenn.edu

1

Abstract. We present a computational analysis of basic Kerberos and Kerberos with public-key authentication (PKINIT) in which we consider authentication and key secrecy properties. Our proofs rely on the Dolev-Yao style model of Backes, P?tzmann and Waidner, which allows for mapping results obtained symbolically within this model to cryptographically sound proofs if certain assumptions are met. This is the most complex fragment of an industrial protocol that has yet been veri?ed at the computational level. Considering a recently ?xed version of PKINIT, we extend symbolic correctness results we previously attained in the Dolev-Yao model to cryptographically sound results in the computational model.

1

Introduction

Cryptographic protocols have traditionally been veri?ed in one of two ways: the ?rst, known as the Dolev-Yao or symbolic approach, abstracts cryptographic concepts into an algebra of symbolic messages [25]; the second, known as the computational or cryptographic approach, retains the concrete view of messages as bitstrings and cryptographic operations as algorithmic mappings between bitstrings, while drawing security de?nitions from complexity theory [16,26,27].

Backes was partially supported by the German Research Foundation (DFG) under grant 3194/1-1. Cervesato was partially supported by ONR under Grant N0001401-1-0795. Jaggard was partially supported by NSF Grants DMS-0239996 and CNS0429689, and by ONR Grant N00014-05-1-0818. Scedrov was partially supported by OSD/ONR CIP/SW URI “Software Quality and Infrastructure Protection for Diffuse Computing” through ONR Grant N00014-01-1-0795 and OSD/ONR CIP/SW URI “Trustworthy Infrastructure, Mechanisms, and Experimentation for Di?use Computing” through ONR Grant N00014-04-1-0725. Additional support from NSF Grants CNS-0429689 and CNS-0524059. Tsay was partially supported by ONR Grant N00014-01-1-0795 and NSF grant CNS-0429689.

D. Gollmann, J. Meier, and A. Sabelfeld (Eds.): ESORICS 2006, LNCS 4189, pp. 362–383, 2006. c Springer-Verlag Berlin Heidelberg 2006

Cryptographically Sound Security Proofs for Basic and Public-Key Kerberos

363

While proofs in the computational approach (with its much more comprehensive adversary model) entail stronger security guarantees, veri?cation methods based on the Dolev-Yao abstraction have become e?cient and robust enough to tackle large commercial protocols, often even automatically [1,15,18,34]. Kerberos, a widely deployed protocol that allows a user to authenticate herself to multiple end servers based on a single login, constitutes one of the most important examples that have been formally analyzed so far within the DolevYao approach. Kerberos 4, which was then the prevalent version, was veri?ed using the Isabelle theorem prover [15]. The currently predominant version, Kerberos 5 [39], has been extensively analyzed using the Dolev-Yao approach.This analysis of Kerberos 5 showed that: a detailed speci?cation of the core protocol enjoys the expected authentication and secrecy properties except for some relatively innocuous anomalies [18]; “cross-realm” authentication in Kerberos is correct when compared against its speci?cation but has weaknesses in practice [21]; and discovered a serious attack against the then-current speci?cation of the public-key extension (PKINIT) of Kerberos [20]. The discovery of the attack on PKINIT led to an immediate correction of the speci?cation and a security bulletin and patch for Microsoft Windows [36]. The proofs for both Kerberos 5 as well as the ?xes to PKINIT are restricted to the Dolev-Yao approach, and currently there does not exist a theorem which allows for carrying the results of existing proofs of Kerberos over to the cryptographic domain with its much more comprehensive adversary. Thus, despite the extensive research dedicated to the Kerberos protocol, and despite its tremendous importance in practice, it is still an open question whether an actual implementation of Kerberos based on provably secure cryptographic primitives is secure under cryptographic security de?nitions. We close this gap (at least partially) by providing the ?rst security proof of the core aspects of the Kerberos protocol in the computational approach. More precisely, we show that core parts of Kerberos 5 are secure against arbitrary active attacks if the Dolev-Yao-based abstraction of the employed cryptography is implemented with actual cryptographic primitives that satisfy the commonly accepted security notions under active attacks, e.g., IND-CCA2 for public-key encryption. Obviously, establishing a proof in the computational approach presupposes dealing with cryptographic details such as computational restrictions and error probabilities, hence one naturally assumes that our proof heavily relies on complexity theory and is far out of scope of current proof tools. However, our proof is not performed from scratch in the cryptographic setting, but based on the Dolev-Yao style model of Backes, P?tzmann, and Waidner [8,12,13] (called the BPW model henceforth), which provides cryptographically faithful symbolic abstractions of cryptographic primitives, i.e., the abstractions can be securely implemented using actual cryptography. Thus our proof itself is symbolic in nature, but refers to primitives from the BPW model. Kerberos is the largest and most complex protocol whose cryptographic security has so far been inferred from a proof in this Dolev-Yao style approach. Earlier proofs in this

364

M. Backes et al.

approach were mainly for small examples of primarily academic interest, e.g., the Needham-Schroeder-Lowe, the Otway-Rees, and the Yahalom protocols [4,7,11]; some similar work has been done on industrial protocols, e.g., [29], although none that are as complex as Kerberos. We furthermore analyze the recently ?xed version of PKINIT and derive computational guarantees for it from a symbolic proof based on the BPW model. Finally we also draw some lessons learned in the process, which highlight areas where to focus research in order to simplify the veri?cation of large commercial protocols with computational security guarantees. In particular it would be desirable to devise suitable proof techniques based on the BPW model for splitting large protocols into smaller pieces which can then be analyzed modularly while still retaining the strong link between the Dolev-Yao and the computational approach. 1.1 Related Work

Early work on linking Dolev-Yao models and cryptography [2,3,28] only considered passive attacks, and therefore cannot make general statements about protocols. A cryptographic justi?cation for a Dolev-Yao model in the sense of simulatibility [40], i.e., under active attacks and within arbitrary surrounding interactive protocols, was ?rst given in [12] with extensions in [8,13]. Based on that Dolev-Yao model, the well-known Needham-Schroeder-Lowe, Otway-Rees, and Yahalom protocols were proved secure in [4,7,11]. All these protocols are considerably simpler than Kerberos, which we analyze in this paper, and arguably of much more limited practical interest. Some work has been done on industrial protocols, such as 802.11i [29], although Kerberos is still a much more complex protocol. Laud [33] has presented a cryptographic underpinning for a Dolev-Yao model of symmetric encryption under active attacks. His work is directly connected with a formal proof tool, but it is speci?c to certain con?dentiality properties and protocol classes. Herzog et al. [30] and Micciancio and Warinschi [35] have also given a cryptographic underpinning under active attacks. Their results are narrower than those in [12] since they are speci?c for public-key encryption and certain protocol classes, but consider slightly simpler real implementations. Cortier and Warinschi [22] have shown that symbolically secret nonces are also computationally secret, i.e., indistinguishable from a fresh random value given the view of a cryptographic adversary. Backes and P?tzmann [9] and Canetti and Herzog [19] have established new symbolic criteria for proving a key cryptographically secret. We stress that none of this work is comprehensive enough to infer computational security guarantees of Kerberos based on an existing symbolic proof; either they are missing suitable cryptographic primitives or rely on slightly changed symbolic abstractions, e.g., as in [12]. Finally, there is also work on formulating syntactic calculi for dealing with probability and polynomial-time considerations and encoding them into proof tools, in particular [17,23,32,37]. This is orthogonal to the work of justifying Dolev-Yao models.

Cryptographically Sound Security Proofs for Basic and Public-Key Kerberos

365

1.2

Structure of the Paper

We start in Sect. 2 with a review of Kerberos and its public-key extension PKINIT. In Sect. 3, we recall the Dolev-Yao style model of Backes, P?tzmann, and Waidner (e.g., [6,8,13,14]), and apply it to the speci?cation of Kerberos 5 and Public-key Kerberos (i.e., Kerberos with PKINIT). Section 4 proves security results for these protocols and lift them to the computational level. Finally, Sect. 5 summarizes this e?ort and outlines areas of future work.

2

Kerberos 5 and Its Public-Key Extension

The Kerberos protocol [38,39] allows a legitimate user to log on to her terminal once a day (typically) and then transparently access all the networked resources she needs for the rest of that day. Each time she wants to, e.g., retrieve a ?le from a remote server, a Kerberos client running on her behalf securely handles the required authentication. The client acts behind the scenes, without any user intervention. Kerberos comprises three subprotocols: the initial round of authentication, in which the client obtains a credential that might be good for a full day; the second round of authentication, in which she presents her ?rst credential in order to obtain a short-term credential (?ve-minute lifetime) to use a particular network service; and the client’s interaction with the network service, in which she presents her short-term credential in order to negotiate access to the service. In the core speci?cation of Kerberos 5 [39], all three subprotocols use symmetric (shared-key) cryptography. Since the initial speci?cation of Kerberos 5, the protocol has been extended by the de?nition of an alternate ?rst round which uses asymmetric (public-key) cryptography. This new subprotocol, called PKINIT [31], may be used in two modes: “public-key encryption mode” and “Di?e-Hellman (DH) mode.” In recent work [20], we showed that there was an attack against the then-current draft speci?cation of PKINIT when publickey encryption mode was used and then symbolically proved the security of the speci?cation as it was revised in response to our attack. Here we study both basic Kerberos (without PKINIT) and the public-key mode of PKINIT as it was revised to prevent our attack. Kerberos Basics. The client process—usually acting for a human user—interacts with three other types of principals when using Kerberos 5 (with or without PKINIT). The client’s goal is to be able to authenticate herself to various application servers (e.g., email, ?le, and print servers). This is done by obtaining a “ticket-granting ticket” (TGT) from a “Kerberos Authentication Server” (KAS) and then presenting this to a “Ticket-Granting Server” (TGS) in order to obtain a “service ticket” (ST), the credential that the client uses to authenticate herself to the application server. A TGT might be valid for a day, and may be used to obtain several STs for many di?erent application servers from the TGS, while a single ST is valid for a few minutes (although it may be used repeatedly) and is used for a single application server. The KAS and the TGS are together known as the “Key Distribution Center” (KDC).

366

M. Backes et al.

C n1 ? ? C, T, n1

KAS

-?

?

C, TGT , {AK, n1 , tK , T }kC

?

AK, tK

Fig. 1. Message Flow in the Traditional AS Exchange, where TGT = {AK, C, tK }kT

The client’s interactions with the KAS, TGS, and application servers are called the Authentication Service (AS), Ticket-Granting (TG), and Client-Server (CS) exchanges, respectively. We will describe the AS exchange separately for basic Kerberos and PKINIT; as PKINIT does not modify the other subprotocols, we only need to describe them once. The Traditional AS Exchange. The abstract structure of the AS exchange is given in Fig. 1. A client C generates a fresh nonce n1 and sends it, together with her own name and the name T of the TGS for whom she desires a TGT, to the KAS K. This message is called the AS REQ message [39]. The KAS responds by generating a fresh authentication key AK for use between the client and the TGS and sending an AS REP message to the client. Within this message, AK is sent back to the client in the encrypted message component {AK, n1 , tK , T }kC ; this also contains the nonce from the AS REQ, the KAS’s local time tK , and the name of the TGS for whom the TGT was generated. (The AK and tK to the right of the ?gure illustrate that these values are new between the two messages.) This component is encrypted under a long-term key kC shared between C and the KAS; this key is usually derived from the user’s password. This is the only time that this key is used in a standard Kerberos run because later exchanges use freshly generated keys. AK is also included in the ticket-granting ticket sent alongside the message encrypted for the client. The TGT consists of AK, C, tK , where tK is K’s local time, encrypted under a long-term key kT shared between the KAS and the TGS named in the request. The computational model we use here does not support timestamps, so we will treat these as nonces; this does not compromise our analysis as the timestamps that we include here are used like nonces. Once the client has received this reply, she may undertake the Ticket-Granting exchange. It should be noted that the actual AS exchange, as well as the other exchanges in Kerberos, is more complex than the abstract view given here. We refer the reader to [39] for the complete speci?cation of Kerberos 5, [31] for the speci?cation of PKINIT, and [18] for a formalization of Kerberos at an intermediate level of detail. The AS Exchange in PKINIT. PKINIT [31] is an extension to Kerberos 5 that uses public key cryptography to avoid shared secrets between a client and KAS; it modi?es the AS exchange but not other parts of the basic Kerberos 5

Cryptographically Sound Security Proofs for Basic and Public-Key Kerberos

367

C n1 , ? n2 , tC ?

KAS Cert C , [tC , n2 ]skC , C, T, n1 { {Cert K , [k, ck]skK } pkC , C, TGT , {AK, n1 , tK , T }k }

-?

k, AK tK ? ?

Fig. 2. Message ?ow in the ?xed version of PKINIT, where TGT = {AK, C, tK }kT

protocol. The long-term shared key (kC ) in the traditional AS exchange is typically derived from a password, which limits the strength of the authentication to the user’s ability to choose and remember good passwords; PKINIT does not use kC and thus avoids this problem. Furthermore, if a public key infrastructure (PKI) is already in place, PKINIT allows network administrators to use it rather than expending additional e?ort to manage users’ long-term keys as in traditional Kerberos. In PKINIT, the client C and the KAS possess independent public/secret key pairs, (pkC , skC ) and (pkK , skK ), respectively. Certi?cate sets Cert C and Cert K issued by a PKI independent from Kerberos are used to testify of the binding between each principal and her purported public key. This simpli?es administration as authentication decisions can now be made based on the trust the KDC holds in just a few known certi?cation authorities within the PKI, rather than keys individually shared with each client (local policies can, however, still be installed for user-by-user authentication). Dictionary attacks are defeated as user-chosen passwords are replaced with automatically generated asymmetric keys. PKINIT resembles the basic AS exchange in that the KAS generates a fresh key AK for the client and TGS to use, and then the KAS transmits AK and the TGT to the client. In public-key encryption mode, attacked and ?xed in [20] and now analyzed here, the key pairs are used for both signature and encryption. The latter is designed to (indirectly) protect the con?dentiality of AK, while the former ensures its integrity. Figure 2 illustrates the AS exchange when the ?xed version (which defends against the attack of [20]) of PKINIT is used. Here we use [m]sk for the digital signature of message m with secret key sk, { }pk for the encryption of m with {m} the public key pk, and {m}k for the encryption of m with the symmetric key k. The ?rst line of Fig. 2 shows our formalization of the AS REQ message that a client C sends to a KAS K when using PKINIT. The last part of the message— C, T, n1 —is exactly as in the traditional AS REQ. The new data added by PKINIT are the client’s certi?cates CertC and her signature (with her secret key skC ) over a timestamp tC and another nonce n2 . The second line in Fig. 2 shows our formalization of K’s response, which is more complex than in basic Kerberos. The last part of the message—C, T GT, {AK, n1 , tK , T }k —is very similar to K’s reply in basic Kerberos; the di?erence is that the symmetric key k protecting AK is now freshly generated by K and is not a long-term shared key. Because k is freshly generated for the reply, it

368

M. Backes et al.

C n3 ? ? TGT , {C, tC }AK , S, n3

TGS

-?

?

C, ST , {SK, n3 , tT , S}AK

?

SK, tT

Fig. 3. Message ?ow in the TGS exchange, where TGT = {AK, C, tK }kT and ST = {SK, C, tT }kS

must be communicated to C before she can learn AK. PKINIT does this by } adding the message { {Cert K , [k, ck]skK } pkC . This contains K’s certi?cates and his signature, using his secret key skK , over k and a keyed hash ck (‘checksum’ in the language of [39]) taken over the entire request from C using the key k; all of this is encrypted under C’s public key pkC . The keyed hash ck binds this response to the client’s request and was added in response to the attack we discovered and reported in [20]. The Later Exchanges. After the client C has obtained the key AK and the TGT, either through the basic AS exchange or the PKINIT AS exchange, she then initiates the TGS exchange, shown in Fig. 3. The ?rst line shows our formalization of the client’s request, called a TGS REQ message; it contains the TGT (which is opaque to the client), an authenticator {C, tC }AK , the name of the server S for which C desires a service ticket, and C’s local time. Once the TGS receives this message, he decrypts the TGT to learn AK and uses this to decrypt the authenticator. Assuming his local policies for granting a service ticket are satis?ed (while we do not model these here, they might include whether the request is su?ciently fresh), the TGS produces a fresh key SK for C and S to share and sends this back to the client in a TGS REP message. The form of this message is essentially the same as the AS REP message from the KAS to C: it contains a ticket (now the service ticket, or ST, {SK, C, tT }kS instead of the TGT) encrypted for the next server (now S instead of T ) and encrypted data for C (now encrypted under AK instead of kC ). Finally, after using the AS exchange to obtain the key SK and the ST, the client may use the CS exchange to authenticate herself to the end server. Figure 4 shows this exchange, including the optional reply from the server that authenticates this server to the client. The client C starts by sending a message (AP REQ) that is similar to the TGS REQ message of the previous round: in contains the (service) ticket and an authenticator ({C, tC }SK ) that is encrypted under the key contained in the ST. The server S simply responds with an AP REP message {tC }SK containing the timestamp from the authenticator encrypted under the key from the ST. Attack on PKINIT. The attack that we found against the then-current speci?cation of PKINIT was reported in [20]. This attack was possible because, at

Cryptographically Sound Security Proofs for Basic and Public-Key Kerberos

369

C ? ? ST , {C, tC }SK

S

-?

?

{tC }SK

?

Fig. 4. Message ?ow in the CS exchange, where ST = {SK, C, tT }kS

the time, the reply from the KAS to the client contained [k, n2 ]skK in place of [k, ck]skK . In particular, the KAS did not sign any data that depended upon the client’s name. This allowed an attacker to copy a message from C to the KAS, use this data in her own request to the KAS, read the reply from the KAS, and then send this reply to C as though it was generated by the KAS for C (instead of for the attacker). The e?ect of this attack was that the attacker could impersonate the later servers (TGS and application servers) to the client, or she could let the client continue the authentication process while the attacker gains knowledge of all new keys shared by the client and various servers. In the latter variation, the client would be authenticated as the attacker and not as C. Security Properties. We now summarize the security properties that we prove here at the symbolic level for both basic Kerberos and Kerberos with PKINIT; the implications on the computational level are discussed in the subsequent sections. We have proved similar properties in symbolic terms using a formalization in MSR for basic Kerberos [18] and for the AS exchange when PKINIT is used [20]. The ?rst property we prove here concerns the secrecy of keys, a notion that is captured formally as Def. 1 in Sect. 4. This property may be summarized as follows. Property 1 (Key secrecy). For any honest client C and honest server S, if the TGS T generates a symmetric key SK for C and S to use (in the CS-exchange), then the intruder does not learn the key SK. The second property we study here concerns entity authentication, formalized as Def. 2 in Sect. 4. This property may be summarized as follows. Property 2 (Authentication properties). i. If a server S completes a run of Kerberos, apparently with C, then earlier: C started the protocol with some KAS to get a ticket-granting ticket and then requested a service ticket from some TGS. ii. If a client C completes a run of Kerberos, apparently with server S, then S sent a valid AP REP message to C. Theorem 1 below shows that these properties hold for our symbolic formalizations of basic and public-key Kerberos in the BPW model. Theorem 2 shows

370

M. Backes et al.

that the authentication property holds as well for cryptographic implementations of these protocols if provably secure primitives are used; the standard cryptographic de?nition of key secrecy however turns out not to hold for cryptographic implementations of Kerberos, which we further investigate below. Because authentication can be shown to hold for Kerberos with PKINIT, it follows that at the level of cryptographic implementation, the ?xed speci?cation of PKINIT does indeed defend against the attack reported in [20].

3

3.1

The BPW Model

Review of the BPW Model

The BPW model introduced in [14] o?ers a deterministic Dolev-Yao style formalism of cryptographic protocols with commands for a vast range of cryptographic operations such as public-key, symmetric encryption/decryption, generation and veri?cation of digital signatures as well as message authentication codes, and nonce generation. Every protocol participant is assigned a machine (an I/O automaton), which is connected to the machines of other protocol participants and which executes the protocol for its user by interacting with the other machines (see Fig. 5). In this reactive scenario, semantics is based on state, i.e., of who already knows which terms. The state is here represented by an abstract “database” and handles to its entries: Each entry (denoted D[j]) of the database has a type (e.g., “signature”) and pointers to its arguments (e.g., “private key” and “message”). This corresponds to the way Dolev-Yao terms are represented. Furthermore, each entry in the abstract database also comes with handles to participants who have access to that entry. These handles determine the state. The BPW model does not allow cheating: only if a participant has a handle to the entry D[j] itself or to the right entries that could produce a handle to D[j] can the participant learn the term stored in D[j]. For instance, if the BPW model receives a command, e.g., from a user machine, to encrypt a message m with key k, then it makes a new abstract database entry for the ciphertext with a handle to the participant that sent the command and pointers to the message and the key as arguments; only if a participant has handles to the ciphertext and also to the key can the participant ask for decryption. Furthermore, if the BPW model receives the same encryption command a second time then it will generate a new (di?erent) entry for the ciphertext. This meets the fact that secure encryption schemes are necessarily probabilistic. Entries are made known to other participants by a send command, which adds handles to the entry. The BPW model is based on a detailed model of asynchronous reactive systems introduced in [40] and is represented as a deterministic machine THH (also an I/O automaton), called trusted host, where H ? {1, . . . , n} denotes the set of honest participants out of all m participants. This machine executes the commands from the user machines, in particular including the commands for cryptographic operations. A system consists of several possible structures. A structure ? consists of a set M of connected correct user machines and a subset S of the free

Cryptographically Sound Security Proofs for Basic and Public-Key Kerberos

371

SH

KA_outu? KA_inu!

H

KA_outS? KA_inS!

KA_outu! KA_inu?

U

KA_outS! KA_inS?

MU

Outu? Outu!

Inu!

OutS?

MS

InS!

OutK?

MK

InK! InK?

MT

OutT? InT! OutT! InT? Outa Ina

Inu?

OutS!

InS?

THH

OutK!

A

Fig. 5. Overview of the Kerberos symbolic system

ports, i.e., S is the user interface of honest users. In order to analyze the security ? of a structure (M , S), an arbitrary probabilistic polynomial-time user machine H is connected to the user interface S and a polynomial-time adversary machine A is connected to all the other ports and H. This completes a structure into a con?guration of the system (see Fig. 5). The machine H represents all users. A con?guration is a runnable system, i.e., for each security parameter k, which determines the input lengths (including the key length), one gets a well-de?ned probability space of runs. To guarantee that the system is polynomially bounded in the security parameter, the BPW model maintains length functions on the entries of the abstract database. The view of H in a run is the restriction to all inputs and outputs that H sees at the ports it connects to, together with its internal states. Formally one de?nes the view viewconf (H) of H for a con?guration conf to be a family of random variables Xk where k denotes the security parameter. For a given security parameter k, Xk maps runs of the con?guration to a view of H. Corresponding to the BPW model, there exists a cryptographic implementation of the BPW model and a computational system, in which honest participants also operate via handles on cryptographic objects. However, the objects are now bitstrings representing real cryptographic keys, ciphertexts, etc., acted upon by interactive polynomial-time Turing machines (instead of the symbolic machines and the trusted host). The implementation of the commands now uses provably secure cryptographic primitives according to standard cryptographic de?nitions (with small additions like type tagging and additional randomization). In [8,12,13,14] it was established that the cryptographic implementation of the BPW model is at least as secure as the BPW model, meaning that whatever an active adversary can do in the implementation can also be achieved by another adversary in the BPW model, or the underlying cryptography can be broken. More formally, a system Sys 1 being at least as secure as another system Sys 2 means that for all probabilistic polynomial-time user H, for all probabilistic polynomial-time adversary A1 and for every computational structure ? (M1 , S) ∈ Sys 1 , there exists a polynomial-time adversary A2 on a corresponding ? symbolic structure (M2 , S) ∈ Sys 2 such that the view of H is computationally

372

M. Backes et al.

indistinguishable in both con?gurations. This captures the cryptographic notion of reactive simulatability. 3.2 Public-Key Kerberos in the BPW Model

We now model the Kerberos protocol in the framework of [14] using the BPW model. We write “:=” for deterministic assignment, “=” for testing for equality and “←” for probabilistic assignment. The descriptions of the symbolic systems of Kerberos 5 and PKINIT are very similar, with the di?erence that the user machines follow di?erent algorithms for the two protocols. We denote Kerberos with PKINIT by “PK,” and basic Kerberos by “K5.” If we let Kerb∈{PK, K5} then, as described in Sect. 3.1, for each user u ∈ {1, . . . , n} there is a protocol machine MKerb which executes the u protocol for u. There are also protocol machines for the KAS K and the TGT T , denoted by MKerb and MKerb . Furthermore, if S1 , . . . , Sl are the servers in K T T ’s ‘realm1 ’, then there are server machines MKerb for S ∈ {S1 , . . . , Sl }. Each S user machine is connected to the user via ports: A port for outputs to the user and a port for inputs from the user, labeled KA outu ! and KA inu ?, respectively (“KA” for“Key sharing and Authentication”). The ports for the server machines are labeled similarly (see Fig. 5). The behavior of the protocol machines is described in detail in [5]. In the following, we comment on two algorithms of PKINIT (Fig. 6 and Fig. 7) . If, for instance, a protocol machine MPK receives a message (new prot, PK, K, T ) at u KA inu ? then it will execute Algorithm 1A (Fig. 6) to start a protocol run. We give a description below. The state of the protocol machine MKerb consists of u the bitstring u and the sets N onceu , N once2u , T GT icket, and Session KeysSu , in which MKerb stores nonces, ticket-granting tickets, and the session keys for u server S, respectively. This is the information a client needs to remember during a protocol run. Only the machines of honest users u ∈ {1, . . . , n} and honest servers S ∈ {S1 , . . . , Sl } will be present in the protocol run, in addition to the machines for K and T . The others are subsumed in the adversary. We denote by H ? {1, . . . , n, K, T, S1 , . . . , Sl } the honest participants, i.e., for v ∈ H the machine MKerb is v guaranteed to run correctly. And we assume that KAS K and TGS T are always honest, i.e., K, T ∈ H. Furthermore, given a set H of honest participants, with {K, T } ? H ? {1, . . . , n, K, T, S1 , . . . , Sl } the user interface of public-key Kerberos will be the set SH := {KA outu !, KA inu ? | u ∈ H \ {K, T }}. The symbolic system is ? the set SysKerb, symb := {(MH , SH )}. Note that, since we are working in an asynchronous system, we are replacing protocol timestamps by arbitrary messages that we assume are known to the participants generating the timestamps (e.g. nonces). All algorithms should immediately abort if a command to the BPW model yields an error, e.g., if a decryption request fails.

1

I.e., administrative domain; we do not consider cross-realm authentication here, although it has been analyzed symbolically in [21].

Cryptographically Sound Security Proofs for Basic and Public-Key Kerberos

373

Notation. The entries of the database D are all of the form (ind, type, arg, hndu1 ,. . . , hndum , hnda , len), where H = {u1 , . . . , um }. We denote by ↓ an error element available to all ranges and domains of all functions and algorithms. So, e.g., hnda =↓ means the adversary does not have a handle to the entry. For entries x ∈ D, the index x.ind ∈ IN DS consecutively numbers all entries in D. The set IN DS is isomorphic to N and is used to distinguish index arguments. We write D[i] for the selection D[ind = i], i.e., it is used as a primary key attribute of the database. The entry x.type ∈ typeset = {auth, cert, enc, nonce, list, pke, pkse, sig, ske, skse,} identi?es the type of x. Here ske/pke is a private/public key pair and skse is a symmetric key which comes with a ‘public’ key pkse. This “public key identi?er” pkse cannot be used for any cryptographic operation but works as a pointer to skse instead (see [7] for a more detailed explanation) . The entry x.arg = (a1 , . . . , aj ) is a possibly empty list of arguments. Many values ai are in IN DS. x.hndu ∈ HN DS ∪ {↓} for u ∈ H ∪ {a} are handles by which u knows this entry. We always use a superscript “hnd ” for handles. x.len ∈ N0 denotes the “length” of the entry; it is computed by applying length functions (mentioned in Sect. 3.1). Initially, D is empty. THH has a counter size ∈ IN DS for the current size of D. For the handle attributes, it has counters currhndu initially 0. First we need to add the symmetric keys shared exclusively by K and T , S and T . Public-key Kerberos uses certi?cates; therefore, in this case all users need to know the public key for certi?cate authorities and have their own public-key certi?cates signed by a certi?cate authority. For simplicity we use only one certi?cate authority CA. Therefore, we add to D an entry for the public key of CA with handles to all users (i.e., to all user machines). For every user we add an entry for the certi?cate of that user signed by the certi?cate authority with a handle to the user (machine). In the case of Kerberos 5, we are adding entries for the key ku shared exclusively by K and u, for all users u. Example of Algorithms. Due to space constraints we are only going to examine PKINIT (Fig. 2) and explain the steps of its Algorithms 1A and 2 (Fig. 6 and Fig. 7) which are more complex than the algorithms in Kerberos 5. For details on the de?nition of the used commands see [8,13,14]. For readability of the ?gures, we noted on the right (in curly brackets) to which terms in the more commonly used Dolev-Yao notation the terms in the algorithms correspond (≈). Protocol start of PKINIT. In order to start a new PKINIT protocol, user u inputs (new prot, PK, K, T ) at port KA inu ?. Upon such an input, MPK runs u Algorithm 1A (Fig. 6) which prepares and sends the AS REQ to K using the BPW model. MPK generates symbolic nonces in steps 1A.1 and 1A.2 by sending u the command gen nonce(). In step 1A.3 the command list( , ) concatenates tu and nu,2 into a new list that is signed in step 1A.4 with u’s private key. Since we are working in an asynchronous system, the timestamp tu is approximated by some arbitrary message (e.g., by a nonce). The command store( ) in step 1A.5–6 makes entries in the database for the names of u and T . Handles for the names u and T are returned, which are added to a list in the next step. MPK stores u

374

M. Backes et al.

A) Input:(new prot, PK, K, T ) at KA inu ? . 1. 2. 3. 4. 5. 6. 7. 8. 9. nu,1 thnd ← gen nonce() u nhnd ← gen nonce() u,2 lhnd ← list(thnd , nhnd ) u u,2 shnd ← sign(skehnd , lhnd ) u uhnd ← store(u) T hnd ← store(T ) mhnd ← list(certhnd , shnd , uhnd , T hnd , nhnd ) 1 u u,1 N onceu := N onceu ∪ {(nhnd , mhnd , K)} u,1 1 send i(K, mhnd ) 1

{l ≈ (tC , n2 )} {s ≈ [tC , n2 ]skC } {m1 ≈ Cert C , [tC , n2 ]skC , C, T, n1 }

B) Input:(continue prot, PK, T, S, AK hnd ) at KS inu ? for S ∈ {S1 , ..., Sl } 1. 2. 3. 4. 5. 6. 7. 8. 9. if ( (T GT hnd , AK hnd , T ) ∈ T GT icketu ) then Abort end if z hnd ← list(uhnd , thnd ) u authhnd ← sym encrypt(AK hnd , z hnd ) nhnd ← gen nonce() u,3 N once2u := N once2u ∪ {nhnd , T, S)} u,3 mhnd ← list(T GT hnd , authhnd , S hnd , nhnd ) 2 u,3 send i(T, mhnd ) 2

{z ≈ C, tC } {auth ≈ {C, tC }AK } {m2 ≈ TGT , {C, tC }AK , S, n3 }

Fig. 6. Algorithm 1 of Public-key Kerberos: Evaluation of inputs from the user (starting the AS and TG exchanges)

information in the set N onceu , which it will need later in the protocol to verify the message authentication code sent by K. In step 1A.8 N onceu is updated. Finally, in step 1A.9 the AS REQ is sent over an insecure (“i” for insecure) channel. Behavior of the KAS K in PKINIT. Upon input (v, K, i, mhnd ) at port outK ? with v ∈ {1, .., n}, the machine MPK runs Algorithm 2 (Fig. 7) which ?rst K checks if the message m is a valid AS REQ and then prepares and sends the corresponding AS REP. In order to verify that the input is a possible AS REQ, the types of the input message m’s components are checked in steps 2.1–2.5. The command retrieve(xhnd ) in step 2.3 returns the bitstring of the entry D[hndu = i xhnd ]. Next the machine veri?es the received certi?cate x1 of v by checking i the signature of the certi?cate authority CA (steps 2.6–2.10). Then the machine extracts the public key pkev out of v’s certi?cate with the command pk of cert( ) and uses this public key to verify the signature x2 received in the AS REQ (steps 2.11–2.16). In steps 2.17–2.21 the types of the message components of the signed message y1 are checked, as well as the freshness of the nonce y12 by comparison to nonces stored in N once3K . If the nonce is fresh then it will be stored in the set N once3K in step 2.23 for freshness checks in future protocol runs. Finally, in steps 2.24–2.36 MPK generates two symmetric keys k and AK, composes the K AS REP, and sends it to v over an insecure channel.

Cryptographically Sound Security Proofs for Basic and Public-Key Kerberos Input:(v, K, i, mhnd ) at outK ? with v ∈ {1, ..., n}. 1. 2. 3. 4. 5. 6. 7. 8. 9. 10. 11. 12. 13. 14. 15. 16. 17. 18. 19. 20. 21. 22. 23. 24. 25. 26. 27. 28. 29. 30. 31. 32. 33. 34. 35. 36. 37. 38. 39.

375

xhnd ← list proj(mhnd , i) for i = 1, ..., 5 i {x1 ≈ CertC , x2 ≈ [tC , n2 ]skC , x5 ≈ n1 } typei ← get type(xhnd ) for i = 1, 2, 5 i {x3 ≈ C, x4 ≈ T } xi ← retrieve(xhnd ) for i = 3, 4 i if (type1 = cert) ∨ (type2 = sig) ∨ (type5 = Nonce) ∨ (x3 = v)∨ (x4 = T ) then Abort end if v hnd ← store(v) b ← verify cert(pkehnd , xhnd , v hnd ) 1 CA if b = f alse then Abort end if pkehnd ← pk of cert(pkehnd , xhnd ) v 1 CA type6 ← get type(pkehnd ) v if (type6 = pke) then Abort end if hnd {y1 ≈ tC , n2 } y1 ← msg of sig(xhnd ) 2 hnd {x2 ≈ [tC , n2 ]skC } b ← verify(xhnd , pkehnd , y1 ) 2 v if b = f alse then Abort end if hnd hnd {y11 ≈ tC , y12 ≈ n2 } y1i ← list proj(y1 , i) for i = 1, 2 hnd type12 ← get type(y12 ) hnd if (type12 = nonce) ∨ ((y12 , .) ∈ N once3K ) then Abort end if hnd N once3K := N once3K ∪ {(y12 , v)} khnd ← gen symenc key() AK hnd ← gen symenc key() {auth ≈ ck} authhnd ← auth(khnd , mhnd ) hnd {z1 ≈ k, ck} z1 ← list(khnd , authhnd ) hnd {s2 ≈ [k, ck]skK } shnd ← sign(skehnd , z1 ) 2 K hnd {z2 ≈ CertK , [k, ck]skK } z2 ← list(certhnd , shnd ) 2 K hnd {m21 ≈ {{CertK , [k, ck]skK }}pkC } m21 ← encrypt(pkehnd , z2 ) K hnd {z3 ≈ AK, C, tK , T } z3 ← list(AK hnd , xhnd , thnd ) 3 K hnd {T GT ≈ {AK, C, tK }kT } T GT hnd ← sym encrypt(sksehnd4 , z3 ) K,x hnd {z4 ≈ AK, n1 , tK , T } z4 ← list(AK hnd , xhnd , thnd , xhnd ) 5 4 K hnd m24 ≈ {Ak, n1 , tK , T }k } m24 ← sym encrypt(khnd , z4 ) mhnd ← list(mhnd , xhnd , T GT hnd , mhnd ) 2 21 3 24 {m2 ≈ {{CertK , [k, ck]skK }}pkC , C, T GT, {Ak, n1 , tK , T }k } 40. send i(v, mhnd ) 2 Fig. 7. Algorithm 2 of Public-key Kerberos: Behavior of the KAS

376

M. Backes et al.

4

4.1

Formal Results

Security in the Symbolic Setting

In order to use the BPW model to prove the computational security of Kerberos, we ?rst formalize the respective security properties and verify them in the BPW model. We ?rst prove that Kerberos keeps the symmetric key, which the TGS T generated for use between user u and server S, symbolically secret from the adversary. In order to prove this, we show that Kerberos also keeps the keys generated by KAS K for the use between u and the TGS T secret. Furthermore, we prove entity authentication of the user u to a server S (and subsequently entity authentication of S to u). This form of authentication is weaker than the authentication Kerberos o?ers, since we do not consider the purpose of timestamps in Kerberos. (Recall that timestamps are currently not included in the BPW model.) Secrecy and Authentication Requirements. We now de?ne the notion of key secrecy, which was informally captured already in Property 1 of Sect. 2, as the following formal requirement in the language of the BPW model. De?nition 1 (Key secrecy requirement). For Kerb ∈{PK, K5} the secrecy Sec requirement ReqKerb is: For all u ∈ H ∩ {1, . . . , n}, and S ∈ H ∩ {S1 , . . . , Sl }, and t1 , t2 , t3 ∈ N: (t1 : KA outS ! (ok, Kerb, u, SK hnd) ∨ t2 : KA outu ! (ok, Kerb, S, SK hnd ) ? t3 : D[hndu = SK hnd ].hnda =↓ where t : D denotes the contents of database D at time t. Similarly t : p?m and t : p!m denotes that message m occurs at input (respectively output) port p at time t. As above PK refers to Public-key Kerberos and K5 to Kerberos 5. In the next section Thm. 1 will show that the symbolic Kerberos systems speci?ed in Sect. 3.2 satisfy this notion of secrecy, and therefore Kerberos enjoys Property 1. Next we de?ne the notion of authentication in Property 2 in the language of the BPW model. De?nition 2 (Authentication requirements). For Kerb ∈ {P K, K5}:

Auth1 i. The authentication requirement ReqKerb is: For all v ∈ H ∩ {1, . . . , n}, for all S ∈ H ∩ {S1 , . . . , Sl }, and K, T :

? t3 ∈ N. t3 : KA outS ! (ok, Kerb, v, SK hnd ) ? ? t1 , t2 ∈ N with t1 < t2 < t3 . t2 : KA inv ! (continue prot, Kerb, T, S, ·) ∧ t1 : KA inv ! (new prot, Kerb, K, T )

Auth2 ii. The authentication requirement ReqKerb is: For all u ∈ H ∩ {1, . . . , n}, for all S ∈ H ∩ {S1 , . . . , Sl }, and K, T :

? t2 ∈ N. t2 : KA outu ! (ok, Kerb, S, SK hnd) ? ? t1 ∈ N with t1 < t2 . t1 : KA inS ! (ok, Kerb, u, SK hnd)

Cryptographically Sound Security Proofs for Basic and Public-Key Kerberos

Auth iii. The overall authentication ReqKerb for protocol Kerb is: Auth Auth1 Auth2 ReqKerb := ReqKerb ∧ ReqKerb

377

Theorem 1 will show that this notion of authentication is satis?ed by the symbolic Kerberos system. Therefore Kerberos has Property 2. When proving that Kerberos has these properties, we will use the notion of a system Sys perfectly ful?lling a requirement Req, Sys |=perf Req. This means the property Req holds with probability one over the probability space of runs for a ?xed security parameter (as de?ned in Sect. 3.1). Later we will also need the notion of a system Sys computationally ful?lling a requirement Req, Sys |=poly Req, i.e., the property holds with negligible error probability for all polynomially bounded users and adversaries (again, over the probability space of all runs for a ?xed security parameter). In particular, perfect ful?llment implies computational ful?llment. In order to prove Thm. 1, we ?rst need to prove a number of auxiliary properties (previously called invariants in, e.g., [4,11]). Although these properties are nearly identical for Kerberos 5 and Public-key Kerberos, their proofs had to be carried out separately. We consider it interesting future work to augment the BPW model with proof techniques that allow for conveniently analyzing security protocols in a more modular manner. In fact, a higher degree of modularity would simplify the proofs for each individual protocol as it could exploit the highly modular structure of Kerberos; moreover, it would also simplify the treatment of the numerous optional behaviors of this protocol. Some of the key properties needed in the proof of Thm. 1, which formalizes Properties 1 and 2, make authentication and con?dentiality statements for the ?rst two rounds of Kerberos. These properties are described in English below; they are formalized and proved in [5]. i) Authentication of KAS to client and Secrecy of AK: If a user u receives a valid AS REP message then this message was indeed generated by K for u and an adversary cannot learn the symmetric keys contained in this message. ii) TGS Authentication of the TGT: If a TGS T receives a TGT and an authenticator {v, tv }AK where the key AK and the username v are contained in the TGT, then the TGT was generated by K and the authenticator was created by v. iii) Authentication of TGS to client and Secrecy of SK: If a user u receives a valid TGS REP then it was generated by T for u and S and no adversary can learn the session key SK contained in this message. iv) Server Authentication of the ST: If a server S receives an ST and an authenticator {v, tv }SK where the key SK and the name v are contained in the ST, then the ST was generated by T and the authenticator was created by v. We can now capture the security of Kerberos in the BPW model in the following theorem, which says that Properties 1 and 2 hold symbolically for Kerberos.

378

M. Backes et al.

We show a proof excerpt in the case of Public-key Kerberos (the outline is analogous for Kerberos 5). Theorem 1. (Security of the Kerberos Protocol based on the BPW Model) – Let SysK5, symb be the symbolic Kerberos 5 system de?ned in Sect. 3.2, and Sec Auth let ReqK5 and ReqK5 be the secrecy and authentication requirements de?ned K5, symb Sec Auth |=perf ReqK5 ∧ ReqK5 . above. Then Sys PK, symb Sec – Let Sys be the symbolic Public-key Kerberos system, and let ReqP K Auth and ReqP K be the secrecy and authentication requirements de?ned above. Sec Auth Then SysPK, symb |=perf ReqP K ∧ ReqP K . Proof (sketch). We assume that all parties are honest. If user u successfully terminates a session run with a server S, i.e., there was an output (ok, PK, S, k hnd ) at KA outu !, then the key k was stored in the set Session KeysSu . This implies that the key was generated by T and sent to u in a valid TGS REP. By auxiliary property iv), an adversary cannot learn k. The case that S successfully termiSec nates a session run is analogous. This shows the key secrecy property ReqP K . Auth1 As for the authentication property ReqP K , if server S successfully terminates a session with u, i.e., there was an output (ok, PK, u, k hnd ) at KA outS !, then S must have received a ticket generated by T (for S and u) and also a matching authenticator generated by user u (by auxiliary property iv)). But the ticket will only be generated if u sends the appropriate request to T , i.e., there was an input (continue prot,PK, T , S, AK hnd ) at KA inu ?. The request, on the other hand, contains a TGT that was generated by K for u (by auxiliary property ii)), therefore u must have sent an request to K. In particular, there had been an input (new prot, PK, K, T ) at KA inu ?. As for the authentication property Auth2 ReqP K , if the user u successfully terminates a session with server S, i.e., there was an output (ok, PK, S, k hnd ) at KA outu !, then it must have received a message encrypted under k that does not contain u’s name. The key k was contained in a valid TGS REP and was therefore generated by T , by auxiliary property iii). Only T , u, or S could know the key k, but only S uses this key to encrypt and send a message that u received. On the other hand, S follows sending such a message immediately by an output (ok, PK, u, k hnd ) at KA outS !. This proof shares similarities with the Dolev-Yao style proofs of analogous properties for Kerberos 5 and PKINIT using the MSR framework [18,20]. The two approaches are similar in the sense that both reconstruct a necessary trace backward from an end state, and in that they rely on some form of induction (based on rank/co-rank functions in MSR). In future work, we plan to draw a formal comparison between these two Dolev-Yao encodings of a protocol, and the proof techniques they support. 4.2 Security in the Cryptographic Setting

The results of [14] allow us to take the authentication results in Thm. 1 and derive a corresponding authentication results for a cryptographic implementation

Cryptographically Sound Security Proofs for Basic and Public-Key Kerberos

379

of Kerberos. Just as Property 2 holds symbolically for Kerberos, this shows that it holds in a cryptographic implementation as well. In particular, entity authentication between a user and a server in Kerberos holds with overwhelming probability (over the probability space of runs). However, symbolic results on key secrecy can only be carried over to cryptographic implementations if the protocol satis?es certain additional conditions. Kerberos unfortunately does not ful?ll these de?nitions, and it can easily be shown that cryptographic implementations of Kerberos do not ful?ll the standard notion of cryptographic key secrecy, see below. This yields the following theorem. Theorem 2. (Computational security of the Kerberos protocol) – Let SysK5, comp denote the computational Kerberos 5 system implemented with provable secure cryptographic primitives. Then SysK5, comp |=poly Auth ReqK5 . – Let SysPK, comp denote the computational Public-key Kerberos system implemented with provable secure cryptographic primitives. Then SysPK, comp Auth |=poly ReqP K . Proof (Sketch for public-key Kerberos). By Thm. 1, we know that SysPK, id Auth |=perf ReqP K . And, as we mentioned earlier, the cryptographic implementation of the BPW model (using provably secure cryptographic primitives) is at least as secure as the BPW model, Syscry, comp ≥poly Syscry, id . After checking that sec the “Commitment Problem” does not occur in the protocol, we can use the Preservation of Integrity Properties Theorem from [6] to automatically obtain Thm. 2. The Commitment Problem occurs when keys that have been used for cryptographic work are revealed later in the protocol. If the simulator in [14] (with which one can simulate a computational adversary attack on the symbolic system) learns in some abstract way that e.g. a ciphertext was sent, the simulator generates a distinguishable ciphertext without knowing the symmetric key nor the plaintext. If the symmetric key is revealed later in the protocol then the trouble for the simulator will be to generate a suitable symmetric key that decrypts the ciphertext into the correct plaintext. This is typically an impossible task. In order for the simulation with the BPW model to work, one thus needs to check that the Commitment Problem does not occur in the protocol. As far as key secrecy is concerned, it can be proven that the adversary attacking the cryptographic implementation does not learn the secret key string as a whole. However, it does not necessarily rule out that an adversary will be able to distinguish the key from other fresh random keys, as required by the de?nition of cryptographic key secrecy. This de?nition of secrecy says that an adversary cannot learn any partial information about such a key and is hence considerably stronger than requiring that an adversary cannot obtain the whole key. For Kerberos we can show that the key SK does not satisfy cryptographic key secrecy after the last round of Kerberos, i.e., SK is distinguishable from other fresh random keys. It should also be noted that this key SK is still indistinguishable

380

M. Backes et al.

from random after the second round but before the start of the third round of Kerberos. We have the following proposition. Proposition 1. a) Kerberos does not o?er cryptographic key secrecy for the key SK generated by the TGS T for the use between client C and server S after the start of the last round of Kerberos. b) After the TGS exchange and before the start of the CS exchange the key SK generated by the TGS T is still cryptographically secret. Proof. a) To see that Kerberos does not o?er cryptographic key secrecy for SK after the start of the third round, note that the key SK is used in the protocol for symmetric encryption. As symmetric encryption always provides partial information to an adversary if the adversary also knows the message that was encrypted. An adversary can exploit this to distinguish the key SK as follows: the adversary ?rst completes a regular Kerberos execution between C and S learning the message {C, t }SK encrypted under the unknown key SK. The adversary will also learn a bounded time period T P (of a few seconds) in which the timestamp t was generated. Next a bit b is ?ipped and the adversary receives a key k, where k = SK for b = 0 and k is a fresh random key for b = 1. The adversary now attempts to decrypt {C, t }SK with k yielding a message m. If m = C, t for a timestamp t then the adversary guesses b = 1. If m = C, t for a timestamp t then the adversary checks whether t ∈ T P or not. If t ∈ T P / then the adversary guesses b = 1 otherwise the adversary guesses b = 0. The probability of the adversary guessing correctly is then 1 ? , where is the probability that for random keys k, SK the ciphertext {C, t }SK decrypted with k is C, t with t ∈ T P . Clearly, is negligible (since the length of the time period T P does not depend on the security parameter). Hence, SK is distinguishable and cryptographic key secrecy does not hold. b) However, before the third round has been started the key SK is not only unknown to the adversary but, in particular, SK has not been used for symmetric encryption yet. We can therefore invoke the key secrecy preservation theorem of [9], which states that a key that is symbolically secret and symbolically unused is also cryptographically secret. This allows us to conclude that SK is cryptographically secret from the adversary. For similar reasons, we also have the following proposition Proposition 2. a) Kerberos does not o?er cryptographic key secrecy for the key AK generated by the KAS K for the use between client C and TGS T after the start of the second round of Kerberos. b) After the AS exchange and before the start of the TGS exchange the key AK generated by the KAS K is still cryptographically secret. Finally, we note the following Remark 1. Kerberos allows the client or the server to generate a sub-session key [39]. This optional key, which can then be used for the encryption of further communication between the two parties, is cryptographically secret as it can

Cryptographically Sound Security Proofs for Basic and Public-Key Kerberos

381

be proven symbolically secret and symbolically unused. This proof can easily be conducted symbolically similar to Thm. 1, and then the key secrecy preservation theorem of [10] can be used to automatically obtain a proof of cryptographic key secrecy for the optional sub-key. Note that this preservation theorem could not be used for proving cryptographic key secrecy for the main key as this key is already used within the key exchange protocol.

5

Conclusions and Future Work

In this paper, we have exploited the Dolev-Yao style model of Backes, P?tzmann, and Waidner [8,12,13] to obtain the ?rst computational proof of authentication for the core exchanges of the Kerberos protocol and its extension to public keys (PKINIT). Although the proofs sketched here are conducted symbolically, grounding the analysis on the BPW model automatically lifts the results to the computational level, assuming that all cryptography is implemented using provably secure primitives. Cryptographic key secrecy in the sense of indistinguishability of the exchanged key from a random key could only be established for the optional sub-key exchanged in Kerberos while for the actually exchanged key, cryptographic key secrecy could be proven not to hold. Potentially promising future work includes the augmentation of the BPW model with specialized proof techniques that allow for conveniently performing modular proofs. Such techniques would provide a simple and elegant way to integrate the numerous optional behaviors supported by Kerberos and nearly all commercial protocols; for example, this would facilitate the analysis of DH mode in PKINIT which is part of our ongoing work. We intend to tackle the invention of such proof techniques that are speci?cally tailored towards the BPW model in the near future, e.g., by exploiting recent ideas from [24]. Another potential improvement we plan to pursue in the near future is to augment the BPW model with timestamps; this would in particular allow us to establish authentication properties that go beyond entity authentication [18,20,21]. A further item on our research agenda is to fully understand the relation between the symbolic correctness proof for Kerberos 5 presented here and the corresponding results achieved in the MSR framework [18,20].

References

1. The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. In Proc. of Computer-aided Veri?cation (CAV). Springer, 2005. URL: www.avispa-project.org. 2. M. Abadi and J. J¨rjens. Formal eavesdropping and its computational interpretau tion. In Proc. TACS, pages 82–94, 2001. 3. M. Abadi and P. Rogaway. Reconciling two views of cryptography: The computational soundness of formal encryption. In Proc. 1st IFIP International Conference on Theoretical Computer Science, pages 3–22. Springer LNCS 1872, 2000. 4. M. Backes. A cryptographically sound Dolev-Yao style security proof of the OtwayRees protocol. In Proc. ESORICS, pages 89–108. Springer LNCS 3193, 2004.

382

M. Backes et al.

5. M. Backes, I. Cervesato, A. D. Jaggard, A. Scedrov, and J.-K. Tsay. Cryptographically sound security proofs for basic and public-key Kerberos. IACR Cryptology ePrint Archive, Report 2006/219, http://eprint.iacr.org/, June 2006. 6. M. Backes and C. Jacobi. Cryptographically sound and machine-assisted veri?cation of security protocols. In Proc. 20th STACS, pages 675–686. Springer LNCS 2607, 2003. 7. M. Backes and B. P?tzmann. A cryptographically sound security proof of the Needham-Schroeder-Lowe public-key protocol. Journal on Selected Areas in Communications, 22(10):2075–2086, 2004. 8. M. Backes and B. P?tzmann. Symmetric encryption in a simulatable Dolev-Yao style cryptographic library. In Proc. CSFW’04, pages 204–218, June 2004. 9. M. Backes and B. P?tzmann. Relating symbolic and cryptographic secrecy. IEEE Trans. Dependable Secure Comp., 2(2):109–123, April–June 2005. 10. M. Backes and B. P?tzmann. Relating symbolic and cryptographic secrecy. In Proc. 26th IEEE Symposium on Security & Privacy, pages 171–182, 2005. Extended version in IACR Cryptology ePrint Archive 2004/300. 11. M. Backes and B. P?tzmann. On the cryptographic key secrecy of the stregthened Yahalom protocol. In Proceedings of 21st IFIP SEC’06, To appear. 12. M. Backes, B. P?tzmann, and M. Waidner. A composable cryptographic library with nested operations (extended abstract). In Proc. CCS’03, pages 220–230, 2003. 13. M. Backes, B. P?tzmann, and M. Waidner. Symmetric authentication within a simulatable cryptographic library. In Proc. ESORICS’03, pages 271–290. Springer LNCS 2808, 2003. 14. M. Backes, B. P?tzmann, and M. Waidner. A universally composable cryptographic library. IACR Cryptology ePrint Archive, Report 2003/015, http://eprint.iacr. org/, January 2003. 15. G. Bella and L. C. Paulson. Kerberos Version IV: Inductive Analysis of the Secrecy Goals. In Proc. ESORICS’98, pages 361–375. Springer LNCS 1485, 1998. 16. M. Bellare and P. Rogaway. Entity authentication and key distribution. In Proc. CRYPTO ’93, pages 232–249. Springer LNCS 773, 1994. 17. B. Blanchet. A computationally sound mechanized prover for security protocols. In Proc. 27th IEEE Symposium on Security & Privacy, 2006. 18. F. Butler, I. Cervesato, A. D. Jaggard, and A. Scedrov. An Analysis of Some Properties of Kerberos 5 Using MSR. In Proc. CSFW’02, 2002. 19. R. Canetti and J. Herzog. Universally composable symbolic analysis of cryptographic protocols (the case of encryption-based mutual authentication and key exchange). In Proc. 3rd Theory of Cryptography Conference (TCC), 2006. 20. I. Cervesato, A. D. Jaggard, A. Scedrov, J.-K. Tsay, and C. Walstad. Breaking and ?xing public-key Kerberos. In Proc. WITS’06, 2006. 21. I. Cervesato, A. D. Jaggard, A. Scedrov, and C. Walstad. Specifying Kerberos 5 Cross-Realm Authentication. In Proc. WITS’05, pages 12–26, 2005. 22. V. Cortier and B. Warinschi. Computationally sound, automated proofs for security protocols. In Proc. ESOP-14, pages 157–171, 2005. 23. A. Datta, A. Derek, J. Mitchell, V. Shmatikov, and M. Turuani. Probabilistic polynomial-time semantics for a protocol security logic. In Proc. ICALP, pages 16–29. Springer LNCS 3580, 2005. 24. A. Datta, A. Derek, J. Mitchell, and B. Warinschi. Key exchange protocols: Security de?nition, proof method, and applications. In 19th IEEE Computer Security Foundations Workshop (CSFW 19), Venice, Italy, 2006. IEEE Press. 25. D. Dolev and A. Yao. On the security of public-key protocols. IEEE Trans. Info. Theory, 2(29):198–208, 1983.

Cryptographically Sound Security Proofs for Basic and Public-Key Kerberos

383

26. O. Goldreich, S. Micali, and A. Wigderson. How to play any mental game – or – a completeness theorem for protocols with honest majority. In Proc. STOC, pages 218–229, 1987. 27. S. Goldwasser and S. Micali. Probabilistic encryption. Journal of Computer and System Sciences, 28:270–299, 1984. 28. J. D. Guttman, F. J. Thayer Fabrega, and L. Zuck. The faithfulness of abstract protocol analysis: Message authentication. In Proc. CCS-8, pages 186–195, 2001. 29. C. He and J. C. Mitchell. Security Analysis and Improvements for IEEE 802.11i. In Proc. NDSS’05, 2005. 30. J. Herzog, M. Liskov, and S. Micali. Plaintext awareness via key registration. In Proc. CRYPTO, pages 548–564. Springer LNCS 2729, 2003. 31. IETF. Public Key Cryptography for Initial Authentication in Kerberos, 1996– 2006. Sequence of Internet drafts available from http://tools.ietf.org/wg/ krb-wg/draft-ietf-cat-kerberos-pk-init/. 32. R. Impagliazzo and B. M. Kapron. Logics for reasoning about cryptographic constructions. In Proc. FOCS, pages 372–381, 2003. 33. P. Laud. Symmetric encryption in automatic analyses for con?dentiality against active adversaries. In Proc. Symp. Security and Privacy, pages 71–85, 2004. 34. C. Meadows. Analysis of the internet key exchange protocol using the NRL Protocol Analyzer. In Proc. IEEE Symp. Security and Privacy, pages 216–231, 1999. 35. D. Micciancio and B. Warinschi. Soundness of formal encryption in the presence of active adversaries. In Proc. TCC, pages 133–151. Springer LNCS 2951, 2004. 36. Microsoft. Security Bulletin MS05-042. http://www.microsoft.com/technet/ security/bulletin/MS05-042.mspx, Aug. 2005. 37. J. Mitchell, M. Mitchell, A. Scedrov, and V. Teague. A probabilistic polynominaltime process calculus for analysis of cryptographic protocols (preliminary report). Electronic Notes in Theoretical Computer Science, 47:1–31, 2001. 38. C. Neuman and T. Ts’o. Kerberos: An Authentication Service for Computer Networks. IEEE Communications, 32(9):33–38, Sept. 1994. 39. C. Neuman, T. Yu, S. Hartman, and K. Raeburn. The Kerberos Network Authentication Service (V5), July 2005. http://www.ietf.org/rfc/rfc4120.txt. 40. B. P?tzmann and M. Waidner. A model for asynchronous reactive systems and its application to secure message transmission. In Proc. S&P, pages 184–200, 2001.

更多相关文档:

09 Authentication *Kerberos*_IT/计算机_专业资料。信息...Information *Security* 10 Authentication *Basic* ... a sequence number or a *cryptographic* *key*), ...

noncebased *cryptographic* protocols, is here ... model assumes their private *keys* to be *secure*....4.1 Guarantees about *Kerberos* *Proving* *for* *Kerberos* ...

(1978) An earlier version of the *Kerberos* ...*cryptographic* *key* between two entities Data ...Here theoretical models *and* *security* *proofs* are ...

In order to be *cryptographically* strong, the pseudo-random running *key* must...*proofs* of *security* by analysing some simple schemes based on the notion of...

rfc4982.Support *for* Multiple Hash Algorithms in *Cryptographically* Generated Addresses (CGAs)_信息与通信_工程科技_专业资料。rfc文档 ...

Pre-distribution Scheme *for* MANET *Security*_专业资料...*Kerberos* *and* *public* *key* infrasructure (PKI) ...3) - Maximum hash depth 4) , a *cryptographic* ...

更多相关标签:

相关文档

- Security Models and Proofs for Key Establishment Protocols
- Security proofs for an efficient password-based key exchange
- On the Security of the KMOV Public Key
- rfc4556.Public Key Cryptography for Initial Authentication in Kerberos (PKINIT)
- Piece In Hand Concept for Enhancing the Security of Multivariate Type Public Key Cryptosystems
- Security_and_Kerberos_Authentication_with_K2_Servers_-_CHS
- Public-key encryption in a multi-user setting Security proofs and improvements
- 基于ECC 和USBKEY 的Kerberos 安全改进方案
- Relations Among Notions of Security for Public-Key Encryption Schemes
- Security of Public Key Cryptosystems based on Chebyshev Polynomials

文档资料共享网 nexoncn.com
copyright ©right 2010-2020。

文档资料共享网内容来自网络，如有侵犯请联系客服。email:zhit325@126.com