### Paper Menu >>

### Journal Menu >>

Journal of Information Security, 2010, 1, 56-67 doi:10.4236/jis.2010.12007 Published Online October 2010 (http://www.SciRP.org/journal/jis) Copyright © 2010 SciRes. JIS Extending the Strand Space Method with Timestamps: Part II Application to Kerberos V* Yongjian Li 1,2 , Jun Pang 3 1Chinese Academy of Sciences, Institute of Software Laboratory of Computer Science, Beijing, China 2The State Key Laboratory of Information Security, Beijing, China 3University of Oldenburg Department of Computer Science Safety-critical Embedded Systems, Oldenburg, Germany E-mail: lyj238@ios.ac.cn, jun.pang@informatik.uni-oldenburg.de Received June 23, 2010; revised Sep tember 14, 2010; accepted July 12, 2010 Abstract In this paper, we show how to use the novel extended strand space method to verify Kerberos V. First, we formally model novel semantical features in Kerberos V such as timestamps and protocol mixture in this new framework. Second, we apply unsolicited authentication test to prove its secrecy and authentication goals of Kerberos V. Our formalization and proof in this case study have been mechanized using Isabelle/HOL. Keywords: Strand Space, Kerberos V, Theorem Proving, Verification, Isabelle/HOL 1. Introduction The first version of Kerberos protocol was developed in the mid eighties as part of project Athena at MIT [1]. Over twenty years, different versions of Kerberos protocols have evolved. Kerberos V (Figure 1 and Figure 2) is the latest version released by the Internet Engineering Task Force (IETF) [2]. It is a password- based system for authentication and authorization over local area networks. It is designed with the following aims: once a client authenticates himself to a network machine, the process of obtaining authorization to access another network service should be completely trans- parent to him. Namely, the client only needs enter his password once during the authentication phase. As we introduced in the previous paper [3], there are two novel semantic features in Kerberos V protocol. First, it uses timestamps to prevent replay attacks, so this deficiency of the strand space theory makes it difficult to analyze these protocols. Second, it is divided into three causally related multiple phases: authentication, authorization, and service protocol phases. One phase may be used to retrieve a ticket from a key distribution center, while a second phase is used to present the ticket to a security-aware server. To make matters more complex, Kerbeors uses timestamps to guarantee the recency of these tickets, that is, such tickets are only valid for an interval, and multiple sub-protocol sessions can start in parallel by the same agent using the same ticket if the ticket does not expire. Little work has been done to formalize both the timestamps and protocol mixture in a semantic framework. The aim of this paper is practical. We hope to apply the extended theory in [3] to the analysis of Kerberos V protocol. Kerberos V is appropriate as our case study because it covers both timestamps and protocol mixture semantical features. Structure of the Paper: Section 2 briefly introduces the overview of Kerberos V. Section 3 presents the formalization of Kerberos V. Sections 4 and 5 prove its secrecy and authentication goals. We discuss related work and conclude the paper in Section 6. 2. An Overview of Kerberos V The protocol’s layout and its message exchanging are presented in Figure 1 and Figure 2 separately. In the infrastructure of the Kerberos V protocol, there is a unique authentication server, and some (not necessarily only one) ticket granting servers. The latter assumption is different from that in [4], where only a unique ticket granting server exists. *This is a revised and extended version of the homonymous paper ap- pearing in the Proceedings the Eighth International Conference on Paral- lel and Distributed Computing, Applications and Technologies (PDCAT 2007, IEEE Computer Society). The main modifications have been made on the presentation of the technical material, with the purpose of having full details. The first author is supported by grants (No. 60833001, 60496321, 60421001) from National Natural Science Foundation of Y. J. LI ET AL. Copyright © 2010 SciRes. JIS 57 Figure 1. The layout of Kerberos V. { } } { { } } } { { } } { { 2 1. :, 2. :,,,,,,, 3.:,,,, ,, 4.:, ,,, Tgs Tgs B K authTicket K authK SK seruTick AKasA Tgs KasAA Tgs authK TaA TgsauthK TaKA ATgsATgsauthKTaA tB TgsAA B seruK T → → → → Authentication phase Authorisation Phase 1444442444443 { } } {} {} } { } 3 3 , ,, 5. :,,,,, 6. : B SauthK et SK seruK seruK AB seruK T ABABseruKTA t BA t → → Service Phase 14444244443 Figure 2. Kerberos V: message exchanging. In order to access some network service, the client needs to communicate with two trusted servers Kas and Tgs. Kas is an authentication server (or the key distribution center) and it provides keys for communication between clients and ticket granting servers. Tgs is a ticket granting server and it provides keys for communication between clients and application servers. The full protocol has three phases each consisting of two messages between the client and one of the servers in turn. Messages 2 and 4 are different from those in Kerberos IV [1,4] in that nested encryption has been cancelled. Later we will show that this change does not affect goals of the protocol. Detailed explanation about Kerberos V is delayed to Section 2, where the protocol is formalized in strand space model with our extensions. Here we only give an overview of the general principles to guarantee recency, secrecy and authentication in the design of Kerberos V. For recency, • A regular sender should attach a timestamp to indicate the time when the message is issued; usually such a message is of the form { } , , K tK K, where t is the time, K may be either a session key or long-term key. • When a regular receiver the message { } , , K t K K first he need be ensured of K ’s secrecy to guarantee that the message is not froged by the penetrator. Second he check the recency of the message by comparing the timestamp t with the reception time. More formally, if the receiving node is n , then )( ntime should be no later than ( ) cracktime Kt + , meaning that this message cannot be cracked at ( ) time n , which in turn indicates that the message { } , , K t K K is recent. For an encrypted message { } K h , the secrecy of a part of the plain message h also comes from both the secrecy of K and the recency of the message { } K h itself. That is to say, when a regular receives { } K h at time t , it must be ensured that the aforementioned two conditions must be guaranteed until t . From this, we can see that recency and secrecy are closely related with each other in a timed protocol framework. Unsolicited tests are the main mechanism to guarantee authentication. Because a guarantee of the existence of a regular node can be drawn from an unsolicited test, a regular agent uses unsolicited test to authenticate its regular protocol participant in Kerberos V. Now let us briefly review the main theoretical results in [3], which will be used in this work. For interesting readers, refer to [3] for preliminary definitions. If an agent is not a penetrator then his shared key cannot be penetrated, which is formalized as follows: Axiom 1 If A ∉ Bad , then P K∉ A K . Lemma 1 is the main technique used to reason about authentication guarantee of a node n which is an unsolicited test for an encrypted term of the form { } K h (e.g., the tickets { } , ,, A a K A TgsauthKT , { } , authK A t , and so on). That is to say, regular agents can use an unsolicited test with other properties of the protocol to guarantee that the agent who originates the term { } K h should be an intended regular agent. Lemma 1 (Unsolicited authentication test) B is a given bundle. Let n be an unsolicited test for { } K h . Then there exists a positive regular node m in B such that nm B and { } )( mtermh K ⊏ and { } ) ( ' K mtermh ⊏ / for any node ' m such that mm' B . Let a be an atomic message that uniquely originates at some node n , m be a positive penetrator node in a bundle B such that and ( ) . mterma ⊏ Suppose M is a test suite for a w.r.t. m in the bundle B . A strand’s Y. J. LI ET AL. Copyright © 2010 SciRes. JIS 58 receiving nodes get messages which are all in ( ) , Msynth but a new message, which is not in ( ) Msynth , is sent in the strand, then the strand must be regular because a penetrator strand can not create such a term. Lemma 2 Let m be a positive node in a bundle , B a be an atomic message that uniquely originates at a regular node n , M be a message set such that ( ) ,,,,, B nmaMsuite and ( ) ( ) ' term msynth M ∈ for any node such that , ' m m + ⇒ and ( ) ( ) , term msynth M ∉ then m is regular . We will illustrate these general principles in detail in the next sections when we formalize the semantics and prove secrecy properties of Kerberos V. 3. Formalizing Kerberos V To model the time for a penetrator to break a message encrypted by a long-term shared key or a session key, we define two constants imeshrKcrackt and ktimesessionKcr . The crack time of any regular agent’s long-term shared key is the constant shrKcracktime, Axiom 2 () = shrKcracktime A cracktime K , for any regular agent A in Kerberos V. The crack time of any session key originated by an authentication server is the constant sessionKcrktime. Axiom 3 () =sessionKcrktime cracktime authK , for any session key authK originated by Kas . The trace tr specifications of the regular strands of Kerberos V (see Figure 2) are defined as predicates:1 1) Part I (Authentication Phase) • Ag-I ],,,,,,,[ 101 ttauthTicketTauthKTgsAi a iff { } { { } } 0 1 1 ( , ,,), () =(,,, , ,,) aKA tA Tgs tr itauthTicket A TgsauthKT + − where TGSs ∈ Tgs and imeshrKcrackt 1 ≤− a Tt . • AS ],,,,,[ 10 ttauthKTgsAas iff { } { } { { } + − ),,, ,,,,,,( ),,,,( =)( 1 11 0 A K Tgs K tauthKTgsA tauthKTgsAt TgsAt astr where TGSs ∈ Tgs . In the first phase, when Kas issues the second message { } { { } } ,,,,,, , A Tgs aa K K A TgsauthKTA TgsauthKT , authK is the session key that will be used for the client A to communicate with a ticket grant server Tgs , Kas attaches a T with the message to indicate when this message is sent; if A receives this message at time 1 t , A will check the condition 1 shrKcracktime a t T − ≤ to ensure the recency of this message. At the end of this phase, A obtains a ticket authTicket and the session key authK to communicate with Tgs. 2) Part II (Authorization Phase) • Ag-II ,,,,,,,[ 2S TservKBauthTicketauthKAi ],, 32 ttservTicket iff ∧∃ 21101 .,,,, iittTTgsi a a Ag-I ∧ ],,,,,,,[ 101 ttauthTicketTauthKTgsAi a ( ) { { } { { } 2 2 2 3 ( , ,, ,,), =( ,,, , ,,) authK SauthK t authTicket A tB tr it servTicket A BservKT + − where TGSs ∈ Tgs and imeshrKcrackt 3 ≤− a Tt and ktime.sessionKcr 3 ≤− S Tt • TGS a TBservKauthKTgsAtgs ,,,,,,[ , ],, 100 ttT iff { } { { } { } { { } } + − ),,, ,,,,,,( ),,, ,,,,,,( =)( 1 11 0 0 authK B K authK Tgs K a tservKBA tservKBAt BTA TauthKTgsAt tgstr where TGSs, ∈ Tgs TGSs, ∉ B 1 sessionKcrktime t + ≤ shrKcracktime a T+ . In the second phase, the situation is more complex. Both Tgs and A need to check whether their received messages are recent by the same mechanism. Furthermore, Tgs also need ensure a side condition that 1 sessionKcrktime shrKcracktime a t T+≤ + to guarantee that the application server B only receives a recent service ticket. Informally speaking, this condition means that Tgs can guarantee any authK that he receives can only be compromised later than servK which is associated with the authK . We will comment this side condition in analysis in the third phase. At the end of this phase, A obtains a ticket servTicket and the session key servK to communicate with B . 1 For simplicity, we assume any trace of a regular agent always re spects the time order in Kerberos V protocol, and we do not include this side condition in the trace specifications. Y. J. LI ET AL. Copyright © 2010 SciRes. JIS 59 3) Part III (Service Phase) • Ag-III 34 5 [ ,,,,,] iA servKservTicket tt iff 10 1 223 ,,,,, ,,,,,, a S iTgsauthKTttiauthTicketB Ttt ∃ . ( ) 3 tr i = {{ } ( ) { } ( ) 4 4 5 4 , ,,,, , , servK servK tservTicketA t t t + ∧ − Ag-I 10 1 [ ,,,,,,,] a iA TgsauthKTauthTickettt ∧ Ag-II 2 [ ,,,,,, S iA authKauthTicketBservKT , 2 31223 , , ] servTicket ttiiii ∧ ∧ a a where T gs ∈ TGSs , 5 shrKcracktime a t T−≤ and 5 sessionKcrktime. S t T− ≤ • Apps 40 1 [, , ,,,,,] S appsA B servK TTtt iff ()= tr apps { } { { } } { } 0 4 1 1 ( , ,,,,,,), ( ,,) SservK KB servK tABservKTAT t t − + where 0 sessionKcrktime S t T− ≤ . In the last phase, it is subtle for the application server B to check the recency of the message { } { } { } 4 , ,,,, SservK KB ABservKTA T . From the ticket { } ,,, S K B A B servKT , B knows that Tgs must have issued {} {} { } 4 , ,,,, ,,, S S K authK B ABservKTAB TservKT at time S T . The potential compromise of servK is from the message { } ,,, S authK A B servKT . A penetrator can either directly break { } ,,, S authK A B servKT to obtain servK , or have authK first then decrypt the message { } ,,, S authK A B servKT to obtain servK . Since authK is also a session key which is originated by Kas in an earlier time than s T , the guarantee for the confidentiality of authK is of extreme importance. The corresponding ticket { } , ,, Tgs aK A TgsauthKT is not available for B , B cannot know the creation time of authK . So B cannot directly check whether authK has been compromised. Fortunately, if Tgs can guarantee that any authK which it receives will be compromised later than servK , associated with the authK , then it is enough for B to check 0 sessionKcrktime S t T− ≤ to ensure that the authK has not been compromised. At the end of this stage, A and B authenticate each other, and A can access the service provided by B . The authentication server Kas must obey the following principles to generate a session key authK : • authK must never be known initially to a penetrator, i. e., P K ∉authK ; • authK must be uniquely originated; • authK is a symmetric key; • authK must not be the same as an agent’s long- term shared key. We summarize these principles as the following axiom: Axiom 4 For any authentication server strand as such that 0 1 [,,,,, ] asA TgsauthKtt AS , we have P K ∉authK , authK uniquely originates in ( ,1) as , 1 = authK authK − , and B authK K ≠ for any agent B . A ticket grant server creates the session key servK by three principles, which are similar to those which the authentication server obeys to create the session key authK . Axiom 5 For any ticket grant server strand tgs such that 0 [, ,,,,,,, a tgsA TgsauthKservKBTT T G S 0 1 , ] t t , P K ∉servK , servK uniquely originates in ( ,1) tgs , 1 = servK servK − , and B servK K ≠ for any agent B . In the following two subsections, we verify the secrecy and authentication properties of Kerberos V. We use similar ways for representing these security properties as in [5]. However, we may need formulate secrecy properties with temporal restrictions when we discuss them in a timed framework. A value v is secret for a protocol if for every bundle C of the protocol the penetrator cannot receive v in cleartext until some time t ; that is, there is no node n in C such that () = term nv and ( ) time nt ≤ . For Kerberos V, we mainly discuss the secrecy of a long-term key of a regular agent, and , authK servK issued by servers. Authentication properties are specified as usual: for a participant B (e.g. acting as a responder), for a certain vector of parameters x r , if each time principal B completes a run of the protocol as a responder using x r supposedly with A , then there is a run of the protocol with A acting as an initiator using x r supposedly with B. And this is formalized as follows: there is a responder strand Resp ( x r ) and the i -th node of the strand is in a bundle C , then there is an initiator strand Init ( x r ) and some j -th node of the initiator strand is in C . In order to prove the secrecy of a long-term key A K , we only need use the well-founded induction principle on bundles. But the knowledge closure property on penetrators is needed when we prove the secrecy of some session key authK or servK . For instance, in order to prove the secrecy of authK , we construct a set { }{ } { } ,,,, ,,, A df aa K K Tgs MATgs authKTATgsauthK T= { } | . t authKt ∪ ⊄ Y. J. LI ET AL. Copyright © 2010 SciRes. JIS 60 We will show that for any node m in a Kerberos bundle , B if )( mtermauthK ⊏ and ( ) time m ≤ shrKcracktime, a T + then ( ) term m must be in ( ). synth M Intuitively, this fact holds because both the penetrator and regular strands can only emit a message which is in ( ) synth M . The penetrator can not decrypt or crack the messages { } , ,, A a K A TgsauthKT and { } , ,, aK Tgs A TgsauthKT until time . shrKcracktime, a T + so it can only synthesize any messages which is in ( ); synth M except a unique authentication server strand, any other regular strand can not emit any message which has authK as a subterm until that time. But for the authentication server strand, he can only emit {} {} 1 1 ,, ,,,, , K K Tgs A A TgsauthKtA TgsauthKt which is still in ( ). synth M Our formal proof is by contradiction. If not so, by the well-founded induction principle on B , we have a minimal element m such that )( mtermauthK ⊏ and ( )(). term msynth M ∉ By the knowledge closure property, we can exclude the cases when m is in a penetrator strand. By case analysis on the form of the trace of regular strands, we can also exclude the case when m is in a regular strand. Thus, a contradiction is concluded. In the following two sections, we give the detailed proof on the secrecy and authentication properties to show how to apply the proof techniques aforementioned. Note that we also have formalized all the proofs in Isabelle/HOL, and the proof scripts can be obtained at [6]. The paper proof here can be viewed as a text account of the mechanical proof scripts at [6]. 4. Proving Secrecy Goals In Kerberos V, a long-term key of a regular agent is never sent in the network, so it cannot be compromised. Let B be a bundle of Kerberos V. For any node in the bundle, the long-term key of a regular agent cannot be a part of the term of the node. In order to prove this lemma, we only need the well-founded induction principle on bundles. Lemma 3 Let B ∈ n . If Bad ∉ A , then A Knterm ≠ )( . Proof. Let )}(|{= xtermKxxP Adf ⊏ ∧∈ B We show that P is empty by contradiction. If there is a node Pn ' ∈ , then by the well-foundedness of a bundle, there exists a node m such that m is minimal in P . Namely, B ∈ m , )( mtermK A ⊏ , and for all B ∈ ' m , if mm ' B then )( ' A mtermK ⊏ / . We prove that the sign of m is positive. If −=)(msign , then by upward-closed property of a bundle there must be another node '' m in the bundle B such that +=)( '' msign and mm '' → . This contradicts with the minimality of m . Then m is either in a regular strand or in a penetrator strand. • CASE 1: m is in a regular strand. There are six cases. Here we only analyze the cases when m is in an authentication server strand ∈ as AS ],,,,,[ 10 ttauthKTgsAas or m is in a client strand ∈ i Ag-II ,[i ,A ,authK ,authTicket ,B,servK , S T ,servTicket , 2 t ] 3 t . The other cases are either straightforward or can be analyzed in a similarly. If m is in an authentication server strand such that ∈ as AS ,[ as ,A ,Tgs ,authK , 0 t]. 1 t By inspection on the trace form of the strand, we have ,1)(= asm , ,1)( astermK A ⊏ , and {} {} 1 1 (,1)=, ,,,, ,, K K Tgs A termasA TgsauthKtA TgsauthKt , then { } 1 , ,, AK Tgs KA TgsauthKt ⊏ or { } 1 , ,, A K A KATgsauthKt ⊏ . In both cases, we can conclude that .=authKK A But this contradicts with Axiom 4. If m is in a client strand such that [ , i i ∈ − Ag II ,A ,authK ,authTicket ,B ,servK , S T ,servTicket ], 32 tt . By inspection on the trace form of the client strand, we have ,0)(= im , ,0)(itermK A ⊏ , and { } { } 2 ( ,0) =,,,, authK term iauthTicketA tB then .authTicketK A ⊏ But by the definition of the client strand, there exists some client strand 11 suchthatii a iand Ag- I ,[ 1 i,A ,Tgs ,authK , a T ,authTicket ]., 10 tt From the definition of the strand , we have ,1).( 1 itermauthTicket ⊏ From this and A K ⊏ ,authTicket we have (1) ,1).( 1 itermK A ⊏ From 1 i a ,i we have (2) ,1)( 1 i ⇒ ,0).(i From (1) and (2), we can conclude that m is not minimal in P . This contradicts with the minimality of m . • CASE 2: m is in a penetrator strand p . Here we only analyze the cases when p is either K K (key strand) or hg C , (concatenation). Other cases are either straightforward or can be analyzed in a similar way. - p is K K . We have ,0)(= pm and KK A ⊏ . Then P K ∈KK A = . This contradicts with Axiom 1. - p is hg C , . We have ,2)(= pm ' and { } hgK A , ⊏ . By the definition of ⊏ , we have gK A ⊏ , or hK A ⊏ . If gK A ⊏ , then ,0)( ptermK A ⊏ . This contradicts with the minimality of m . The case when hK A ⊏ can be analyzed similarly. Y. J. LI ET AL. Copyright © 2010 SciRes. JIS 61 If an authentication ticket { } , ,, A a K A TgsauthKT or { } , ,, Tgs aK A TgsauthKT occurs as a subterm of a node in B , A is not compromised, and Tgs is a ticket granting server, then it can be guaranteed that there must be an authentication server strand as in which { } , ,, A a K A TgsauthKT and { } , ,, Tgs aK A TgsauthKT originate at time a T . Therefore, a T is the earliest time when { } , ,, A a K A TgsauthKT and { } , ,, Tgs aK A TgsauthKT occur in B . With the specification of the origination of the key authK by Kas (formulated by Axiom 4), we also are ensured that a T is the earliest time when authK occurs in B . The minimal property of a T will be used in the proof of Lemma 5. Lemma 4 Let B ∈ n , Bad ∉ A , and TGSs ∈ Tgs . If { } , ,, A a K A TgsauthKT or { } ,,,( ) A aK A TgsauthKTtermn ⊏ , then there exists an authentication server strand as such that ,,,[ TgsAasAS ],, 0a TtauthK for some 0 t , B ∈ ,1)( as , and )( ntimeT a ≤ . Proof. Here we only prove the case { } , ,, A a K A TgsauthKT ⊏ ( ) . nterm The other case can be proved in a similar way. First we prove that (1) n is an unsolicited test for the term { } , ,, A a K A TgsauthKT We only need prove that A K must be regular w.r.t. n . By Lemma 3, there is no node m in B such that ( ) ,= A Kmterm so A K must be regular w.r.t. n . From (1), by Lemma 1, there exists a positive regular node m in B such that nm B and { } , ,, A a K A TgsauthKT )( mterm ⊏ and { } , ,, A a K A TgsauthKT ⊏ / )( ' mterm for any node ' m such that mm ' B . From nm B and B is a bundle, we can easily conclude )()( ntimemtime≤ and . B ∈ m Now we prove that m must be in an authentication server strand. From the fact that m is regular, then we have six cases, here we select two cases when m is in an authentication server strand as such that AS as[, ' A , ' Tgs , ' authK , 0 t , 1 ] t or in an ticket granting server strand tgs such that tgs[TGS , ' A ,Tg , ' authK , servK , ' B , ' a T , 0 T , 0 t , ]. 1 t • m is in an authentication server strand as such that AS as[, ' A , ' Tgs , ' authK , 0 t , ]. 1 t By inspection on the form of the strand, ( ) ,1= asm because m is positive. Obviously { }{ } 1 1 ( ) , ,,,, ,, Tgs A '' '''' K K term m A TgsauthKtATgsauthKt ′ ′ = By { } , ,, A a K A TgsauthKT ⊏ ),(mterm we have either (2) { } , ,, A a K A TgsauthKT ⊏ { } 1 , ,, Tgs ' '' K A TgsauthKt ′ or (3) { } , ,, A a K A TgsauthKT ⊏ { } 1 , ,, A ' '' K A TgsauthKt ′ . From (2), we have ' A A = and ' TgsTgs = and ' authKauthK = and 1 =tT a , so AS ].,,,,,[ 0a TtauthKTgsAas Case (3) can be prove similarly. • m is in an ticket granting server strand such that TGS ].,,,,,,,,,[ 100 ttTTBservKauthKTgAtgs ' a ''' By inspection on the form of the strand, ( ) ,1= tgsm because m is a positive node. Obviously { }{} { } 1 1 (),,,,, ,,. B ' '' ' K authK termmABservK tABservK t ′ ′ = From { } , ,, A a K A TgsauthKT ⊏ ),(mterm we have either (2) { } , ,, A a K A TgsauthKT ⊏ { } 1 , ,, B ' ' K ABservK t ′ or (3) { } , ,, A a K A TgsauthKT ⊏ { } 1 , ,, ' ' authK ABservKt ′ . From (2), we can prove that ,= ' BTgs then by the assumption , TGSs ∈ Tgs we have . TGSs ∈ ' B But by the definition of the ticket granting server, we have ∉ ' B TGSs . Therefore a contradiction is obtained. Case (3) can be proved similarly. Once the authentication tickets { } , ,, A a K A TgsauthKT or { } , ,, Tgs aK A TgsauthKT are created by the authentication server Kas at a T , then the session key authK will be not compromised until the time imeshrKcrackt + a T . Lemma 5 Let B ∈ n , Bad ∉ A , and TGSs ∈ Tgs . If { } , ,, A a K A TgsauthKT or { } ,,,( ) Tgs aK A TgsauthKTtermn ⊏ , then for any node B ∈ m such that ( ) a time mT ≤ + shrKcracktime , authKmterm ≠ )( . Proof. First we define two sets. { } { } { } tauthKt TauthKTgsA TauthKTgsA M Tgs K a A K a df ⊏ / ∪ =| ,,, ,,,, ={.()shrKcracktime df a Pm mtimemT ∈ ∧≤+∧ B ( ) ( )} term msynthM ∉ . We show that for any node B ∈ m such that imeshrKcrackt)( +≤ a Tmtime , ( ) Msynthmterm ∈)( . In order to prove this, we only need show P is empty. We prove the assertion by contradiction. If P is not empty , then by the well-foundedness of a bundle, (1) there exists a positive node m such that B ∈ m , ( ) ,)(Msynthmterm ∉ imeshrKcrackt)( +≤ a Tmtime , and for all B ∈ ' m , if mm ' B then ( ) term m ∈ ( ) synth M . First from the fact that { } , ,, A a K A TgsauthKT or { } ,,,( ) Tgs aK A TgsauthKTtermn ⊏ by the Lemma 4, then Y. J. LI ET AL. Copyright © 2010 SciRes. JIS 62 there exists an authentication server strand as such that ,,,[ TgsAas AS ],, 0a TtauthK for some 0 t , B ∈,1)(as , and )(ntimeT a ≤ . From the definition of AS and Axiom 4 , we have (2) authK uniquely originates at ,1)(as and .=,1)( a Tastime Next we prove that (3) ,M suite( ,authK , m ,1),(as B ). Here we need show both { } , ,, A a K A TgsauthKT and { } , ,, Tgs aK A TgsauthKT are components in B . From A ∉ Bad and Tgs ∈ TGSs , by Lemma 3, we have that neither A K nor Tgs K is compromised, and they are symmetry, therefore B ),,( 1 mKregular A − and ),,( 1 B mKregular Tgs − ; furthermore from )(mtime ≤ a T + ,imeshrKcrackt and by Axiom 2, )( A Kcracktime = ime,shrKcrackt with (2), we have )(mtime ≤ + ,1)(astime ,)( A Kcracktime similarly we have )(mtime ≤ ,1)( astime ( ), Tgs cracktime K + so (3) is proved . From (1), we have for any ' m such that mm ' + ⇒, term ( ) Msynthm ' ∈ )( . With (2)(3), by Lemma 2, we have m must be in a regular strand i , then there exist six cases. Here we analyze the cases when AS i[, ' A ,' Tgs , ' authK ,' t 0 , ] 1 t , other cases are more simpler . If m is in an authentication server strand AS i[, ' A ,' Tgs , ' authK ,' t 0 , ]. 1 t By inspection on the form of the strand, ( ) ,1= im because m is positive. Obviously { }{ } 1 1 ( ) ,,,,,,, Tgs A ' ''' '' K K term m A TgsauthKtA TgsauthKt ′ ′ = . Obviously authK ⊏ term ),(m otherwise term )(m ∈ .M Therefore { } 1 , ,, A ' '' K authKATgsauthKt ′ ⊏ or { } 1 , ,, Tgs ' '' K authKATgsauthKt ′ ⊏ then . ' authKauthK = From the definition of Axiom 4, we have authK uniquely originates from the strand i . Combining with (2), we have ias = , then ' A A = , ' TgsTgs = , a Tt = 1 , so { }{} ( ) , ,,,, ,, ( ) a a K K Tgs A term m A TgsauthKTA TgsauthKT synth M = ∈ This contradicts with the fact ).()( Msynthmterm ∉ Therefore for any node B ∈ m such that ≤)(mtime imeshrKcrackt+ a T, ( ) Msynthmterm ∈)( . Next we only need prove that ( ) MsynthauthK ∉. We prove by contradiction, if ( ) ,MsynthauthK ∈ by the rule inversion of definition of synth, we have ,MauthK ∈ this contradicts with the definition of M . In order to prove the conclusion of Lemma 5, we need the conclusion of Lemma 4, which ensures us that a penetrator cannot crack the term { } , ,, a K A A TgsauthKT (or { } ,,, aK Tgs A TgsauthKT) to obtain .authK Because the earliest time when authK occurs in B is a T and authK can only occur in { } , ,, a K A A TgsauthKT (or { } ,,, aK Tgs A TgsauthKT) the penetrator cannot crack such a term until imeshrKcrackt+ a T, and what he can only do is to synthesize some term from M . Therefore, authK must be safe until that time. Furthermore, the intermediate result of this proof tells us that )(mterm must be in ( ) Msynth for any node B ∈ m such that ime.shrKcrackt)(+≤ a Tmtime If both the tickets { } , ,, S authK A B servKT and { } , ,, a K A A TgsauthKT occur as a part of the term of a node in B , A and B are not compromised, and B is not a ticket grant server, and authK is still not compromised at the time when the above two tickets occur, then it can be guaranteed that A must have passed the first and second phases of the protocol, and a ticket grant server strand tgs must exist in B , where two tickets { } , ,, S K B A B servKT and { } , ,, S authK A B servKT are issued for some session key authK. Similar to Lemma 4, this lemma ensures us that S T is the earliest time when servK occurs in B , and this minimal property is needed in the proof of Lemma 7. Lemma 6 Let B ∈ nm,, Bad ∉ A, TGSs ∈ Tgs . If both { } ,,,( ) aKA A TgsauthKTtermm ⊏ , and { } ,,,( ) SauthK A B servKTterm n ⊏ and imeshrKcrackt)( +≤ a Tntime, then there exists a ticket granting server strand tgs such that ,,[ AtgsTGS ],,,,,,, 00 Sa TtTTBservKauthKTgs for some 0 T, 0 t, ,1)(tgs B ∈ and )(ntimeT S ≤. Here we only give the proof sketch of this lemma. First we need show that (1) n is an unsolicited test for { } , ,, S authK A B servKT in B . We need prove ( ) .,, B nauthKregular This can be ensured by Lemma 5. Because ime,shrKcrackt)( +≤ a Tntime we have ( ) ' term nauthK ≠for any node ' nsuch that ()(). ' time ntimen ≤ From (1), we can show that there is a regular node ' n such that ' n n B and { } , ,, SauthK A B servKT ⊏ term )( ' n and Y. J. LI ET AL. Copyright © 2010 SciRes. JIS 63 { } , ,, SauthK A B servKT ⊄ term )( ' m for any node ' m such that '' nm B . By the case analysis on the form of regular strands, we can prove that ' n must be in a ticket granting server strand tgs such that [ , tgs TGS , A , Tgs , authK , servK , B , a T 0 , T 0 , t ] S T for some 0 T, 0 t, ' ntgs=,1)( and )(= ' SntimeT . Moreover, by the fact a ticket { } , ,, S authK A B servKT is originated at time S T, then the session key servK will not be compromised until the time ktimesessionKcr + S T. Because during the interval from S T to ktimesessionKcr + S T, neither { } , ,, S authK A B servKT will be cracked, nor the session key authK can be obtained by a penetrator to decrypt the ticket { } , ,, S authK A B servKT. Lemma 7 Let 0 m, B ∈ n, Bad ∉ BA,, TGSs ∈ Tgs . If both { } , ,, a K A A TgsauthKT )( 0 mterm ⊏ and { } ,,,( ) SauthK A B servKTterm n ⊏ , and imeshrKcrackt)( +≤ a Tntime, then for any node B ∈ m such that ktimesessionKcr)( +≤ S Tmtime , servKmterm ≠ )( . Proof. First we define: { } { } { } .| ,,, ,,,, =tservKt TservKBA TservKBA M authK S B K S df ⊏ / ∪ We will show that for any node B ∈ m such that ktimesessionKcr)( +≤ S Tmtime , term ( ) .)( Msynthm ∈ We prove the assertion by contradiction. Let .{= mP df m ∈ B ∧ )(mtime ≤ S T + ∧ktimesessionKcr term )(m ∉ ( ) }.Msynth If P is not empty , then by the well-foundedness of a bundle, (1) there exists a positive node m such that B ∈ m , )(mtime ≤ S T + ktimesessionKcr , term ( ) ,)( Msynthm ∉ and for all B ∈ ' m , if mm ' B then term ( ) Msynthm ' ∈)( . From the fact { } , ,, a K A A TgsauthKT ),( 0 mterm ⊏ by Lemma 4, there exists an authentication server strand as such that ,,,[ TgsAas AS ],, 0 a TtauthK for some 0 t , B ∈,1)( as . From the definition of AS , we know (2) authK uniquely originates at ,1)(as and a Tastime =,1)( . From the fact that { } , ,, a K A A TgsauthKT ⊏ )( 0 mterm and { } , ,, a K A A TgsauthKT ⊏ ),(nterm by Lemma 6, then there exists a ticket granting server strand tgs such that ,[tgs TGS ,A ,Tgs ,authK ,servK ,B, a T , 0 T , 0 t ] S T for some 0 T , 0 t . From the definition of TGS and Axiom 5, we have (3) servK uniquely originates at ,1)(tgs , ,=,1)( S Ttgstime { } , ,, aKTgs A TgsauthKT ⊏ term ,0),(tgs and imeshrKcracktktimesessionKcr +≤+ aS TT . From { } , ,, aKTgs A TgsauthKT ⊏ term ,0),(tgs by Lemma 4, we can easily conclude that ,0)(tgstimeT a ≤ , then (4) ,1).(tgstimeT a ≤ Next we prove that (5) ),1),(,,,( B tgsmservKMsuite. Here we need show both { } , ,, a K B A TgsservKT and { } , ,, S authK A B servKT are components in B . From Bad ∉ B , by Lemma 3, we have B K are never compromised, similar to counterpart in Lemma 5, we can prove that ( ) .,, 1 B mKregular B − From imeshrKcracktktimesessionKcr +≤+ aS TT and ktimesessionKcr)( +≤ S Tmtime , we have (6) ime,shrKcrackt)(+≤ a Tmtime with (4), we have )(mtime ≤ +,1)(tgstime ).( B Kcracktime From (6) and { } ,,,( ) aKA A TgsauthKTtermm ⊏ for any node ' n such that )( ' ntime ≤ ),(mtime we have ktimesessionKcr)( +≤ S ' Tntime , then )( ' ntime ≤ eshrKcrktim+ a T , by Lemma 5, term )( ' n ≠ ;authK by Axiom 4, authK is symmetry, therefore 1 − authK = ,authK so ( ) .,, 1 B mauthKregular − From ktime,sessionKcr)( +≤ S Tmtime and by Axiom 4 again, we have )(authKcracktime =ktime,sessionKcr then +≤ S Tmtime)(),(authKcracktime with (3), we have ≤)( mtime +,1)( tgstime).( authKcracktime Therefore (5) is proved . From (1), we have for any ' m such that mm '+ ⇒ , term ∈)( ' m synth ( ) M . With (2)(5), by Lemma 2, we have m must be in a regular strand i , then there exists six cases. Here we analyze the cases when ,[i AS , ' A , ' Tgs , ' authK , 0 ' t] 1 t or ,[i TGS , ' A, ' Tgs , ' authK , ' servK , ' B, ' a T, 0 ' T, 0 ' t] ' S T , other cases are more simpler. If ,[i AS , ' A, ' Tgs , ' authK , 0 ' t], 1 t then by inspection on the form of the strand, ( ) ,1= im because m is positive. Obviously { }{ } 1 1 ( ) , ,,,, ,, K' Tgs ' ''' '' KA term m A TgsauthKtA TgsauthKt ′ = . Obviously servK ⊏ term ),(m otherwise ∈)(mterm .M Therefore { } , ,, A ' '' aK servKA TgsauthKT ′ ⊏ or { } , ,, Tgs ' '' aK servKA TgsauthKT ′ ⊏ then servK = . ' authK From Axiom 5, we have authK uniquely originates from the strand i . Combining with (3), we can conclude i is both an authentication server strand and a ticket granting server Y. J. LI ET AL. Copyright © 2010 SciRes. JIS 64 strand, obviously this is a contradiction. If ],,,,,,,,,[ 00 ' S ''' a ''''' TtTTBservKauthKTgsAiTGS , then by similar argument, we can prove that ' servK = ,servK from Axiom 5, we have servK uniquely originates from i , with (3), we have i = tgs , we can prove that { }{ } { } ( ) , ,,,, ,, S S K authK B term m A B servKTA B servK T= then term ∈)(m synth ( ) M this contradicts with (1). At last we only need prove that term ∈)(m synth ( ) M implies that term servKm ≠)( , this is similar to counterpart in Lemma 5. Both Lemma 6 and Lemma 7 have the assumption that { } , ,, a K A A TgsauthKT is a subterm of the node n , which can guarantee that authK must be a session key originated by an authentication server strand. The assumption imeshrKcrackt)( +≤ a Tntime is used to guarantee that authK is still safe at )(ntime . Besides, the two terms { } , ,, S authK A B servKT and { } , ,, a K A A TgsauthKT are intelligible for the client A , so these two lemmas are secrecy properties in the view of A . In Lemmas 6 and 7, both { } , ,, S authK A B servKT and { } , ,, a K A A TgsauthKT are unintelligible for an application server B because authK and A K cannot be known by B . So the two properties are not in B ’s view. B can only receive a message such as { } , ,, S K B A B servKT , can it be ensured that servK is confidential when he receives the message { } , ,, S K B A B servKT ? The following two lemmas are about the confidential information inferred from the message { } , ,, S K B A B servKT . They are secrecy properties in B ’s view. Once a server ticket such as { } , ,, S K B A B servKT occurs in a bundle, where A and B are not compromised, and B is not a ticket granting server, then conclusions similar to those in Lemma 6 and Lemma 7 can be drawn. Lemma 8 Let B ∈ n , Bad ∉ BA, , and TGSs ∉ B . If { } ,,,( ) SKB A B servKTtermn ⊏ , then there exists a ticket grant server strand tgs such that ,,[ AtgsTGS ],,,,,,, 00 Sa TtTTBservKauthKTgs for some Tgs , authK , a T , 0 T , , 0 t B ∈,1)(tgs and )(ntimeT S ≤ . Lemma 9 Let B ∈ n , Bad ∉ BA, , and TGSs ∉ B . If { } ,,,( ) SKB A B servKTtermn ⊏ , then for any node B ∈ m such that ktimesessionKcr)( +≤ S Tmtime , servKmterm ≠)( . Here we summarize the main ideas used in the above proof of secrecy properties. • For a long-term key of a regular agent, its secrecy is easily inferred because it is never sent as a part of a message. We only need the well-founded induction principle on bundles to prove this. • But for a short session key authK or servK , the cases are more complex because they are sent as a part in a message such as { } , ,, a K A A TgsauthKT or { } , ,, S authK A B servKT . In kerberos V, a session key such as authK ( servK ) occurs as a part of a term of node n which is of the form { } K h , where K can be either a long-term key or another short session key, and h also contains a timestamp t such as )( Sa TT , which indicates the time when { } K h is . t As mentioned before, both secrecy of K and recency of { } K h should be guaranteed. Secrecy of K can be directly drawn from other lemmas on K . But for recency checking, firstly we need prove that the timestamp t indeed indicates the time when { } K h is originated. Lemmas 4, 6, 9 play a role in guaranteeing that t is the first time when authK ( servK ) is originated. From this and the assumption that cracktime)( +≤ tntime ( K ), the recency of { } K h can be proved. 5. Proving Authentication Goals For convenience, we call that a strand i uses a term { } K h as an unsolicited test if there is a node n is in the strand i and is an unsolicited test for { } K h in a bundle . B Because a guarantee of the existence of a regular node can be drawn from an unsolicited test, a regular agent uses unsolicited test to authenticate its regular protocol participant in Kerberos V. The client strand in the authentication phase receives { } , ,, a K A A TgsauthKT as an unsolicited test that authenti- cates the positive node of the authentication server strand. The intuition behind this authentication is quite straight- forward. By case analysis on the form of ,i we have { } , ,, aKA A TgsauthKT ⊏ ( ,1), term i combining with the assumption that A is not compromised, by Lemma 4, we have { } , ,, a K A A TgsauthKT can only be originated by an authentication server. For the sake of brevity, in the following discussion we use ],,,[yxP K ∗ to denote ],,,[.yxxPx '' K∃ . B is a bundle of Kerberos V. Lemma 10 Let Bad ∉ A . If i is a client strand in the authentication phase such that Ag-I ,,,,[ authKTgsAi ],,, 10 ttauthTicketT a and B ∈,1)(i , then there exists an authentication server strand as such that ,,[ AasAS ],*,, a TauthKTgs , B ∈,1)(as . The ticket grant server strand uses { } 0 , authK A T as an unsolicited test to authenticate the client strand in the authorization phase. This guarantee is ensured from the secrecy of authK , which is in turn guaranteed by the ticket { } , ,, aK Tgs A B authK T . By the trace specification of a ticket grant server strand, we have that Y. J. LI ET AL. Copyright © 2010 SciRes. JIS 65 {} {} 0 , ,,,, aK authK Tgs ABauthKTA T is received by Tgs earlier than the time ktimesessionKcr+ a T , by Lemma 5, authK is safe at that time. Lemma 11 Let Bad ∉ A , TGSs ∈ Tgs . If tgs is a ticket grant server strand such that [,, tgs A TGS 00 1 ,,,,,,, ], a TgsauthKservKBT Ttt and B ∈,0)(tgs , then there exists a client strand i in the authorization phase such that B ∈,0)(i and Ag-II ],,,,,,,,,,[ 0 ∗∗∗∗∗∗∗ TauthKAi . Proof. By analysis on the form of tgs strand, we have (1) { } 0 , authK A T ⊏ ,0),(tgs (2) { } , ,, aK Tgs A B authK T ⊏ ,0)(tgsterm and ,0)(tgstime ≤ a T + imeshrKcrackt . From (2), by Lemma 5, we have that ( ) ≠mterm authK for any B ∈ m such that ( ) mtime ≤ ,0)(tgstime , therefore ),0),(,( B tgsauthKregular . With (1), by Lemma 1, we have (3) there is a positive regular node m such that ,0)(tgsm B and { } 0 , authK A T ⊏ ( ) term n and { } 0 , authK A T ⊄ )( ' mterm for any node ' m such that .mm ' B Obviously B ∈ m . Now we need prove that m must be in a client strand i in the authorization phase. From the fact that m is regular, then we have six cases, here we select two cases when (4) m is in a strand i such that Ag-II ,[i , ' A, ' authK , ' authTicket , ' B, ' servK , ' S T, ' servTicket , 2 t] 3 t or (5) m is in a strand i such that [ ,,, ' ' i AservK Ag_III ].,, 54 ttservTicket ' Other cases are more simpler. If (4) holds, then m ( ) ,0= i because m is positive. From { } 0 ,( ) authK A Ttermn ⊏ and ( ) mterm = { } { } 2 , ,,, ' authK authTicketA tB we have either (6) { } 0 , ' authK A TauthTicket ⊏ or (7) { } { } 0 2 ,,. ' ' authK authK A TAt ⊏ If (6) holds, then by the definition of the client strand, there exists some client strand 1 1 such that i i a iand Ag-I ,[ 1 i, ' A, ' Tgs , ' authK , ' a T, ' authTicket ]., 10 '' tt From the definition of the strand , we have { } 1 ( ,1),,,,. ''''' aK' A term iauthTicketATgsauthKT = From this and (6), we have (8) { } 0 1 ,( ,1). authK A Ttermi ⊏ From 1 i a ,i ,1)( 1 i ⇒ ,0)(i, then (9),1)( 1 i ,0).(i B But (8) and (9) contradicts with (3). If (7) holds, then ,= ' AA ,=20tT .= ' authKauthK So the conclusion is obtained. If (5) holds, then similar to the counterpart of the argument for case (4), we have either (10) { } 0 , authK A T ⊏ ' servTicket or (11) { } { } 0 4 ,,. ' ' authK servK A TAt ⊏ For case (10), its proof is similar to that of case (6). If (11) holds, then (12),= ' AA ,= 40 tT .= ' servKauthK By the definition of Ag_III , (13) there is a client strand 12 ,ii such that 1 i a 2 i and 2 i a i and Ag-II ,,[ 2 ' Ai , ' authK , ' authTicket , ' B, ' servK , ' S T, ' servTicket , 2 t ] 3 t and Ag-I ,[ 1 i, ' A, ' Tgs , ' authK , ' a T, ' authTicket ], 10 '' tt for some ' Tgs ∈ . TGSs Obviously, { } , ,, A ' '' aK A TgsauthKT ′ ⊏ 1 ( ,1), term i { } 2 ,,,( ,1), ''' ' S' authK ABservKTterm i ⊏ and ime.shrKcrackt,1)( 2 +≤ ' a Titime From 1 i a 2 i and 2 i a i and B ∈,0)(i, we have B ∈,1)(1 i and B ∈,1)(2 i. From (12), and the assumption Bad, ∉ A by Lemma 6, (14) there is a ticket granting server strand ' tgs such that [ , ' tgs TGS , ' A, ' Tgs , ' authK , ' servK , ' B, ' a T, 0 ' T, 0 '' t] ' S T for some .,00 ''' tT But from (2), by Lemma 4, we have (15) there is an authentication server as such that ,,,[ TgsAasAS ,authK ], 0a 'Tt for some . 0 ' t But from (12) and Axioms 4,5, we have astgs'= because authK ( ' servK ) uniquely originates from a strand , obviously this is a contradiction. A client strand 2 i in the authorization phase receives { } , ,, S authK A B servK T as an unsolicited test. Note that { } , ,, S authK A B servK T is received in the second node in the client strand; furthermore, from the definition of Ag-II , we have that there exists a client strand 1 i in the authentication phase such that 1 i a 2 i, and the ticket { } , ,, a K A A TgsauthKT must be received at the second node of 1 i; from the definition of Ag-II , { } , ,, S authK A B servK T must have been received at an earlier time than + a T imeshrKcrackt , then by Lemma 5, it can be guaranteed that authK must be safe at the time when the client strand receives { } , ,, S authK A B servK T. Lemma 12 Let Bad ∉ BA,. If i is a client strand in the authorization phase such that Ag-II [ ,,,, a iA authKT auth -,,1)(and],,,,,, 10 B ∈ittservTicketTservKBTicket S then there exists a client strand 0 i in the authentication phase, and a ticket grant server strand , tgs and some Tgs such that ii a 0 and Ag-I 0 [ ,,,,, a iA TgsauthKT , , ] authTicket ∗ ∗ and [, ,,,, , tgsA TgsauthKservKB TGS , ,,] a s T T ∗ ∗, and B ∈,1)(tgs , and TGSs ∉ B. The application server B receives { } 4 , servK A T, which is an unsolicited test to guarantee that the first received message must be from a client strand in the service phase. This guarantee is ensured from the secrecy of servK , which is in turn guaranteed by the ticket { } , ,, S K B A B servK T. By the trace specification of an application server strand, we have that { } { } { } 4 , ,,,, SservKKB ABservKTA T Y. J. LI ET AL. Copyright © 2010 SciRes. JIS 66 is received by B earlier than the time ktimesessionKcr + S T . By Lemma 9, servK is safe at that time. Lemma 13 Let Bad ∉ BA, , TGSs ∉ B . If b is an application server strand such that [ ,,,, bAB servK Apps 40 1 ,,, ], S TT tt B ∈ ,0)(andb , then there are two client strands 2 i , 3 i and some servTicket such that 2 3 i i a and B ∈ ,0)( 3 i and 2 [ ,,*,*,,, iAB servK Ag_II , , S T servTicket *,*] and 3 [ ,,,, iA servKservTicket Ag_III 4 ,*] T . The client strand in the service phase uses { } 4 servK T as an unsolicited test to authenticate the application server strand. This guarantee is also ensured from the secrecy of servK , which is in turn guaranteed by the ticket { } , ,, S authK A B servK T , and { } , ,, a K A A TgsauthKT . By the trace specification of an application server strand, we have that { } 4 servK T is received by A earlier than the time ktimesessionKcr + S T and imeshrKcrackt + a T . By Lemma 7, servK is safe at that time. Lemma 14 Let Bad ∉ BA, , TGSs ∉ B . If 3 i is a client strand in a service phase such that 3 [ , i Age nt_III ],,,,, 4∗ tservTicketservKA and B ∈ ,1)( 3 i , and 2 i is a client strand in the authorization phase such that 2 [, ,,, ,,,, S iA authKauthTicketBservKTservTicket Agent_II 2 3 , ] t t and 2 3 i i a , then there exists an application server strand b such that 4 ,,,,,[tTservKBAb S Apps , ],, ∗ ∗ and B ∈ ,1)(b . Proof. By analysis on the form of strand 3 i and , 2 i we have (1) ,1)( 3 iterm = { } 4 servK t and (2) { , , A B } , authK servKTs ⊏ ,1)( 2 iterm . By unfolding the definition of Agent_II, there exists a client strand 1 i such that 1 i a 2 i and Ag-I ,[ 1 i,A ,Tgs ,authK , a T ,authTicket , 0 t] 1 t and Tgs ∈ TGSs for some ,Tgs , a T, 0 t. 1 t Obviously, (3) { } , ,, a K A A TgsauthKT ⊏ ,1),( 1 iterm ,1)( 1 itime ≤ a T imeshrKcrackt +. From 1 i a 2 i and 2 i a , 3 i we can easily conclude that ,1)( 1 i + ⇒ ,1)( 3 i and ,1)( 2 i + ⇒ ,1).( 3 i With ,1)( 3 i ∈ B , we have ,1)( 2 i ∈ B and ,1)( 1 i ∈ B . With (2)(3), by Lemma 7, (4) ( ) mterm ≠ servK for any node m such that )(mtime ≤ S TktimesessionKcr +. By the definition of Agent_III, we have (5) ,1)( 3 itime ≤ S T ktime.sessionKcr + From (4)(5), we have ( ) mterm ≠ servK for any node m such that )(mtime ≤ ,1),( 3 itime therefore regular ( ) .,1),(, 3 B iservK So ,1)( 3 i is an unsolicited test for { } 4 servK T in . B By Lemma 1, (5) there is a regular positive node m such that m ,1)( 3 i B and { } 4 servK t ⊏ ( ) mterm and { } 4 authK t ⊏ / )( ' mterm for any node ' m such that ' m.m B Obviously B ∈ m . By simple case analysis, we have that m must be in an application server b such that ,[b Apps , ' A, ' B, ' servK , ' S T, 4 ' t , ∗ ], ∗ ,1).(= bm By the definition of Apps , ,1)(bterm = . 4 ' servK ' t With ,1)( 4 btermt servK ⊏ , we have (6) servKservK ' = and .= 44tt' Let { } { } { } .| ,,, ,,,, =tservKt TservKBA TservKBA M authK S B K S df ⊏ / ∪ Obviously ,0)(btime ,1)(btime B ,1)( 3 itime B ≤ S T + ktimesessionKcr , by the proof of Lemma 7, we have ,0)(bterm ∈ ),(Msynth i.e., { } { } { } 4 , ,,,( ) B ''' ' S'servK K ABservKTtsynth M ′ ′ ′∈. By the definition of synth , we have { } , ,, B ''' ' S ' K A B servKT ′ ∈ ),(Msynth then we have (7) { } , ,, B ' '' ' S ' K A BservKT ′ ∈ M or (8) { } , ,, ''' ' S A B servKT ∈ ).(Msynth If (7) holds, from (6) (7) and the definition of M , we have { } , ,, S A B servK T = { } , ,, ''' ' S A B servKT , then A = ' A and B = ' B and S T = . ' S T Therefore, the conclusion holds. If (8) holds, by the definition of synth, we have ' servK ∈ ),(Msynth with (6), we have servK ∈ ),(Msynth then by the definition of synth, we have servK ∈ ,M but this contradicts with the definition of M . Roughly speaking, we need two steps to prove an authentication goal that if there is a regular responder strand Resp ( r , x r ) and the k -th node of the strand is in a bundle B , then there is an initiator strand Init ( i , x r ) and some j-th node of the initiator strand is in B . First we prove that ),( kr is an unsolicited test for some encrypted term { } K h in B , which requires the secrecy of K . This is can be easily proved by the secrecy results on keys in section 3. Therefore, we have that there exists some regular node m in B by Lemma 2. Second, we need prove that m indeed is the intended node ),(ji . In order to prove this, we need do case analysis on the form of the strand which m possibly lies in. This proof needs unicity property of some session keys and the results of unsolicted tests, namely, the facts that { } K h ⊏ )(mterm and m is minimal. 6. Conclusions and Related Work Our main aim is to extend and mechanize the strand space theory to analyze Kerberos V, since mechanization in a theorem prover not only helps us model protocols rigorously and specify protocol goals without any ambiguity, it also guarantees a formal proof. Besides the Y. J. LI ET AL. Copyright © 2010 SciRes. JIS 67 essential inherence from the classic strand space method, our work is deeply inspired by Paulson and Bella’s work. We have directly used their formalization of message algebra, and have learned a lot about the semantics of timestamps and replay attacks from [4]. However, we model and analyze protocols in strand space theory rather than in Paulson's trace theory. In detail, we model behaviors of all the agents by strands, and mainly use the well-founded induction principle to prove properties. So in our Isabelle formalization, main efforts have been devoted to definitions and lemmas about strand space theory. e.g., we formalize strands, bundles, unique originality, the well-founded principle on bundles, and use this principle to prove important results such as unsolicited authentication test and regularity of keys. In [4], the ability of a penetrator to crack a stale en- crypted message is modelled by the Oops rule in the inductive definition of a trace, and the trace definition depends on the protocol under study. However, in the strand space theory, a penetrator’s abilities are modelled to be independent of the protocol, that is the main reason why we relate a key with a crack time, and model a penetrator’s ability of cracking a stale encrypted message by a new key cracking strand. The advantage of our method is that modelling a penetrator’s behavior remains independent and results such as the unsolicited authen- tication tests can be generalized. Regarding verification of the Kerberos protocols, Mitchell et al. [7] analyzed a simplified version of the protocol by model checking, and Butler et al. [8] analyzed the Kerberos V protocol using MSR [9]. But they did not include timestamps and replay attacks in their model, in fact the former work ignored both nonces and timestamps, and the latter only considered the implementation of the Kerberos protocol basing on nonce. 7. References [1] S. P. Miller, J. I. Neuman, J. I. Schiller and J. H. Saltzer, “Kerberos Authentication and Authorisation System,” Technical Report, Technical Plan Section E.2.1, MIT, Athena, 1989. [2] K. R. C. Neuman and S. Hartman, “The Kerberos Net- work Authentication Service (v5),” Technical report, In- ternet RFC 4120, July 2005. [3] Y. L. and J. Pang, “Extending the Strand Space Method with Timestamps: Part I the Theory,” Journal of Informa- tion Security, Vol. 1, No. 2, 2010, pp. 45-55. [4] G. Bella, “Inductive Verification of Cryptographic Pro- tocols,” PhD Thesis, Cambridge University Computer Laboratory, 2000. [5] F. Javier Thayer, J. C. Herzog and J. D. Guttman, “Strand Spaces: Proving Security Protocols Correct,” Journal of Computer Security, Vol. 7, No. 1, 1999, pp. 191-230. [6] Y. Li, “Strand Space and Security Protocols”. http://lcs. ios.ac.cn/˜lyj238/strand.html. [7] J. C. Mitchell, M. Mitchell and U. Stern, “Automated Analysis of Cryptographic Protocols Using Murphi,” Proceedings of 18th Symposium on Security and Privacy, 1997, pp. 141-153. [8] L. Bozga, C. Ene and Y. Lakhnech, “A Symbolic Deci- sion Procedure for Cryptographic Protocols with Time Stamps,” Journal of Logic and Algebraic Programming, Vol. 65, No. 1, 2005, pp. 1-35. [9] F. Butler, I. Cervesato, A. Jaggard and A. Scedrov, “A formal Analysis of Some Properties of Kerberos 5 Using MSR,” Proceedings of 15th IEEE Computer Security Foundations Workshop, 2002, pp. 175-190. |